This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-nfc

Description: Define the not-free predicate for classes. This is read " x is not free in A ". Not-free means that the value of x cannot affect the value of A , e.g., any occurrence of x in A is effectively bound by a "for all" or something that expands to one (such as "there exists"). It is defined in terms of the not-free predicate df-nf for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Assertion df-nfc ⊢ Ⅎ _ x A ↔ ∀ y Ⅎ x y ∈ A

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 cA class A
2 0 1 wnfc wff Ⅎ _ x A
3 vy setvar y
4 3 cv setvar y
5 4 1 wcel wff y ∈ A
6 5 0 wnf wff Ⅎ x y ∈ A
7 6 3 wal wff ∀ y Ⅎ x y ∈ A
8 2 7 wb wff Ⅎ _ x A ↔ ∀ y Ⅎ x y ∈ A