Theorem dfnfc2

Description: An alternative statement of the effective freeness of a class A , when it is a set. (Contributed by Mario Carneiro, 14-Oct-2016) (Proof shortened by JJ, 26-Jul-2021)

	Ref	Expression
Assertion	dfnfc2	|- ( A. x A e. V -> ( F/_ x A <-> A. y F/ x y = A ) )

Proof

Step	Hyp	Ref	Expression
1		nfcvd	|- ( F/_ x A -> F/_ x y )
2		id	|- ( F/_ x A -> F/_ x A )
3	1 2	nfeqd	|- ( F/_ x A -> F/ x y = A )
4	3	alrimiv	|- ( F/_ x A -> A. y F/ x y = A )
5		df-nfc	|- ( F/_ x { A } <-> A. y F/ x y e. { A } )
6		velsn	|- ( y e. { A } <-> y = A )
7	6	nfbii	|- ( F/ x y e. { A } <-> F/ x y = A )
8	7	albii	|- ( A. y F/ x y e. { A } <-> A. y F/ x y = A )
9	5 8	sylbbr	|- ( A. y F/ x y = A -> F/_ x { A } )
10	9	nfunid	|- ( A. y F/ x y = A -> F/_ x U. { A } )
11		nfa1	|- F/ x A. x A e. V
12		unisng	|- ( A e. V -> U. { A } = A )
13	12	sps	|- ( A. x A e. V -> U. { A } = A )
14	11 13	nfceqdf	|- ( A. x A e. V -> ( F/_ x U. { A } <-> F/_ x A ) )
15	10 14	syl5ib	|- ( A. x A e. V -> ( A. y F/ x y = A -> F/_ x A ) )
16	4 15	impbid2	|- ( A. x A e. V -> ( F/_ x A <-> A. y F/ x y = A ) )