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

Metamath Proof Explorer

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 imbitrid 
 |-  ( 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 ) )