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

Metamath Proof Explorer

Theorem eusvnfb

Description: Two ways to say that A ( x ) is a set expression that does not depend on x . (Contributed by Mario Carneiro, 18-Nov-2016)

Ref Expression
Assertion eusvnfb 
|- ( E! y A. x y = A <-> ( F/_ x A /\ A e. _V ) )

Proof

Step Hyp Ref Expression
1 eusvnf 
 |-  ( E! y A. x y = A -> F/_ x A )
2 euex 
 |-  ( E! y A. x y = A -> E. y A. x y = A )
3 eqvisset 
 |-  ( y = A -> A e. _V )
4 3 sps 
 |-  ( A. x y = A -> A e. _V )
5 4 exlimiv 
 |-  ( E. y A. x y = A -> A e. _V )
6 2 5 syl 
 |-  ( E! y A. x y = A -> A e. _V )
7 1 6 jca 
 |-  ( E! y A. x y = A -> ( F/_ x A /\ A e. _V ) )
8 isset 
 |-  ( A e. _V <-> E. y y = A )
9 nfcvd 
 |-  ( F/_ x A -> F/_ x y )
10 id 
 |-  ( F/_ x A -> F/_ x A )
11 9 10 nfeqd 
 |-  ( F/_ x A -> F/ x y = A )
12 11 nf5rd 
 |-  ( F/_ x A -> ( y = A -> A. x y = A ) )
13 12 eximdv 
 |-  ( F/_ x A -> ( E. y y = A -> E. y A. x y = A ) )
14 8 13 biimtrid 
 |-  ( F/_ x A -> ( A e. _V -> E. y A. x y = A ) )
15 14 imp 
 |-  ( ( F/_ x A /\ A e. _V ) -> E. y A. x y = A )
16 eusv1 
 |-  ( E! y A. x y = A <-> E. y A. x y = A )
17 15 16 sylibr 
 |-  ( ( F/_ x A /\ A e. _V ) -> E! y A. x y = A )
18 7 17 impbii 
 |-  ( E! y A. x y = A <-> ( F/_ x A /\ A e. _V ) )