Metamath Proof Explorer

Theorem eusvnf

Description: Even if x is free in A , it is effectively bound when A ( x ) is single-valued. (Contributed by NM, 14-Oct-2010) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion eusvnf 
|- ( E! y A. x y = A -> F/_ x A )

Proof

Step Hyp Ref Expression
1 euex 
 |-  ( E! y A. x y = A -> E. y A. x y = A )
2 nfcv 
 |-  F/_ x z
3 nfcsb1v 
 |-  F/_ x [_ z / x ]_ A
4 3 nfeq2 
 |-  F/ x y = [_ z / x ]_ A
5 csbeq1a 
 |-  ( x = z -> A = [_ z / x ]_ A )
6 5 eqeq2d 
 |-  ( x = z -> ( y = A <-> y = [_ z / x ]_ A ) )
7 2 4 6 spcgf 
 |-  ( z e. _V -> ( A. x y = A -> y = [_ z / x ]_ A ) )
8 7 elv 
 |-  ( A. x y = A -> y = [_ z / x ]_ A )
9 nfcv 
 |-  F/_ x w
10 nfcsb1v 
 |-  F/_ x [_ w / x ]_ A
11 10 nfeq2 
 |-  F/ x y = [_ w / x ]_ A
12 csbeq1a 
 |-  ( x = w -> A = [_ w / x ]_ A )
13 12 eqeq2d 
 |-  ( x = w -> ( y = A <-> y = [_ w / x ]_ A ) )
14 9 11 13 spcgf 
 |-  ( w e. _V -> ( A. x y = A -> y = [_ w / x ]_ A ) )
15 14 elv 
 |-  ( A. x y = A -> y = [_ w / x ]_ A )
16 8 15 eqtr3d 
 |-  ( A. x y = A -> [_ z / x ]_ A = [_ w / x ]_ A )
17 16 alrimivv 
 |-  ( A. x y = A -> A. z A. w [_ z / x ]_ A = [_ w / x ]_ A )
18 sbnfc2 
 |-  ( F/_ x A <-> A. z A. w [_ z / x ]_ A = [_ w / x ]_ A )
19 17 18 sylibr 
 |-  ( A. x y = A -> F/_ x A )
20 19 exlimiv 
 |-  ( E. y A. x y = A -> F/_ x A )
21 1 20 syl 
 |-  ( E! y A. x y = A -> F/_ x A )