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	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2	0 1	wnfc	⊢ Ⅎ 𝑥 𝐴
3		vy	⊢ 𝑦
4	3	cv	⊢ 𝑦
5	4 1	wcel	⊢ 𝑦 ∈ 𝐴
6	5 0	wnf	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
7	6 3	wal	⊢ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴
8	2 7	wb	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )