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	\|- ( F/_ x A <-> A. y F/ x y e. A )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	\|- x
1		cA	\|- A
2	0 1	wnfc	\|- F/_ x A
3		vy	\|- y
4	3	cv	\|- y
5	4 1	wcel	\|- y e. A
6	5 0	wnf	\|- F/ x y e. A
7	6 3	wal	\|- A. y F/ x y e. A
8	2 7	wb	\|- ( F/_ x A <-> A. y F/ x y e. A )