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