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

Metamath Proof Explorer

Theorem eusv2nf

Description: Two ways to express single-valuedness of a class expression A ( x ) . (Contributed by Mario Carneiro, 18-Nov-2016)

Ref Expression
Hypothesis eusv2.1 
|- A e. _V
Assertion eusv2nf 
|- ( E! y E. x y = A <-> F/_ x A )

Proof

Step Hyp Ref Expression
1 eusv2.1 
 |-  A e. _V
2 nfeu1 
 |-  F/ y E! y E. x y = A
3 nfe1 
 |-  F/ x E. x y = A
4 3 nfeuw 
 |-  F/ x E! y E. x y = A
5 1 isseti 
 |-  E. y y = A
6 19.8a 
 |-  ( y = A -> E. x y = A )
7 6 ancri 
 |-  ( y = A -> ( E. x y = A /\ y = A ) )
8 5 7 eximii 
 |-  E. y ( E. x y = A /\ y = A )
9 eupick 
 |-  ( ( E! y E. x y = A /\ E. y ( E. x y = A /\ y = A ) ) -> ( E. x y = A -> y = A ) )
10 8 9 mpan2 
 |-  ( E! y E. x y = A -> ( E. x y = A -> y = A ) )
11 4 10 alrimi 
 |-  ( E! y E. x y = A -> A. x ( E. x y = A -> y = A ) )
12 nf6 
 |-  ( F/ x y = A <-> A. x ( E. x y = A -> y = A ) )
13 11 12 sylibr 
 |-  ( E! y E. x y = A -> F/ x y = A )
14 2 13 alrimi 
 |-  ( E! y E. x y = A -> A. y F/ x y = A )
15 dfnfc2 
 |-  ( A. x A e. _V -> ( F/_ x A <-> A. y F/ x y = A ) )
16 15 1 mpg 
 |-  ( F/_ x A <-> A. y F/ x y = A )
17 14 16 sylibr 
 |-  ( E! y E. x y = A -> F/_ x A )
18 eusvnfb 
 |-  ( E! y A. x y = A <-> ( F/_ x A /\ A e. _V ) )
19 1 18 mpbiran2 
 |-  ( E! y A. x y = A <-> F/_ x A )
20 eusv2i 
 |-  ( E! y A. x y = A -> E! y E. x y = A )
21 19 20 sylbir 
 |-  ( F/_ x A -> E! y E. x y = A )
22 17 21 impbii 
 |-  ( E! y E. x y = A <-> F/_ x A )