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 )