Metamath Proof Explorer

Theorem 2sb5ndALT

Description: Equivalence for double substitution 2sb5 without distinct x , y requirement. 2sb5nd is derived from 2sb5ndVD . The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in 2sb5ndVD . (Contributed by Alan Sare, 19-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2sb5ndALT 
|- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 ax6e2ndeq 
 |-  ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
2 anabs5 
 |-  ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
3 2pm13.193 
 |-  ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )
4 3 exbii 
 |-  ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. y ( ( x = u /\ y = v ) /\ ph ) )
5 hbs1 
 |-  ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph )
6 id 
 |-  ( A. x x = y -> A. x x = y )
7 axc11 
 |-  ( A. x x = y -> ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
8 6 7 syl 
 |-  ( A. x x = y -> ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
9 pm3.33 
 |-  ( ( ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph ) /\ ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ) -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
10 5 8 9 sylancr 
 |-  ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
11 hbs1 
 |-  ( [ v / y ] ph -> A. y [ v / y ] ph )
12 11 sbt 
 |-  [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
13 sbi1 
 |-  ( [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph ) -> ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph ) )
14 12 13 ax-mp 
 |-  ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
15 id 
 |-  ( -. A. x x = y -> -. A. x x = y )
16 axc11n 
 |-  ( A. y y = x -> A. x x = y )
17 16 con3i 
 |-  ( -. A. x x = y -> -. A. y y = x )
18 15 17 syl 
 |-  ( -. A. x x = y -> -. A. y y = x )
19 sbal2 
 |-  ( -. A. y y = x -> ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) )
20 18 19 syl 
 |-  ( -. A. x x = y -> ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) )
21 imbi2 
 |-  ( ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) -> ( ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph ) <-> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ) )
22 21 biimpac 
 |-  ( ( ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph ) /\ ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) ) -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
23 14 20 22 sylancr 
 |-  ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
24 10 23 pm2.61i 
 |-  ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
25 24 nf5i 
 |-  F/ y [ u / x ] [ v / y ] ph
26 25 19.41 
 |-  ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
27 4 26 bitr3i 
 |-  ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
28 27 exbii 
 |-  ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) <-> E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
29 nfs1v 
 |-  F/ x [ u / x ] [ v / y ] ph
30 29 19.41 
 |-  ( E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
31 28 30 bitr2i 
 |-  ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
32 31 anbi2i 
 |-  ( ( E. x E. y ( x = u /\ y = v ) /\ ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
33 2 32 bitr3i 
 |-  ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
34 pm5.32 
 |-  ( ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) <-> ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. x E. y ( x = u /\ y = v ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ) )
35 33 34 mpbir 
 |-  ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
36 1 35 sylbi 
 |-  ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )