Metamath Proof Explorer

Theorem 2sb5ndVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd is 2sb5ndVD without virtual deductions and was automatically derived from 2sb5ndVD . (Contributed by Alan Sare, 30-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )
2:1: |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. y ( ( x = u /\ y = v ) /\ ph ) )
3:: |- ( [ v / y ] ph -> A. y [ v / y ] ph )
4:3: |- [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
5:4: |- ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
6:: |- (. -. A. x x = y ->. -. A. x x = y ).
7:: |- ( A. y y = x -> A. x x = y )
8:7: |- ( -. A. x x = y -> -. A. y y = x )
9:6,8: |- (. -. A. x x = y ->. -. A. y y = x ).
10:9: |- ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph )
11:5,10: |- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
12:11: |- ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
13:: |- ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph )
14:: |- (. A. x x = y ->. A. x x = y ).
15:14: |- (. A. x x = y ->. ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
16:13,15: |- (. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
17:16: |- ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
19:12,17: |- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
20:19: |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
21:2,20: |- ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
22:21: |- ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) <-> E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
23:13: |- ( 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 ) )
24:22,23: |- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
240:24: |- ( ( 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 ) ) )
241:: |- ( ( 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 ) )
242:241,240: |- ( ( 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 ) ) )
243:: |- ( ( 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 ) ) ) )
25:242,243: |- ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
26:: |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
qed:25,26: |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )

Ref Expression
Assertion 2sb5ndVD 
|- ( ( -. 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 idn1 
 |-  (. 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 e1a 
 |-  (. A. x x = y ->. ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
9 imim1 
 |-  ( ( [ 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 e01 
 |-  (. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
11 10 in1 
 |-  ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
12 hbs1 
 |-  ( [ v / y ] ph -> A. y [ v / y ] ph )
13 12 sbt 
 |-  [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
14 sbi1 
 |-  ( [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph ) -> ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph ) )
15 13 14 e0a 
 |-  ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
16 idn1 
 |-  (. -. A. x x = y ->. -. A. x x = y ).
17 axc11n 
 |-  ( A. y y = x -> A. x x = y )
18 17 con3i 
 |-  ( -. A. x x = y -> -. A. y y = x )
19 16 18 e1a 
 |-  (. -. A. x x = y ->. -. A. y y = x ).
20 sbal2 
 |-  ( -. A. y y = x -> ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) )
21 19 20 e1a 
 |-  (. -. A. x x = y ->. ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) ).
22 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 ) ) )
23 22 biimpcd 
 |-  ( ( [ 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 ) ) )
24 15 21 23 e01 
 |-  (. -. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
25 24 in1 
 |-  ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
26 11 25 pm2.61i 
 |-  ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
27 26 nf5i 
 |-  F/ y [ u / x ] [ v / y ] ph
28 27 19.41 
 |-  ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
29 4 28 bitr3i 
 |-  ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
30 29 exbii 
 |-  ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) <-> E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
31 5 nf5i 
 |-  F/ x [ u / x ] [ v / y ] ph
32 31 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 ) )
33 30 32 bitr2i 
 |-  ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
34 33 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 ) ) )
35 2 34 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 ) ) )
36 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 ) ) ) )
37 35 36 mpbir 
 |-  ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
38 1 37 sylbi 
 |-  ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )