Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2sb5ndVD Structured version   Visualization version   Unicode version
Theorem 2sb5ndVD 39146
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 38785) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd 38776 is 2sb5ndVD 39146 without virtual deductions and was automatically derived from 2sb5ndVD 39146. (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 ) ) )
Assertion
Ref Expression
2sb5ndVD |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
Distinct variable groups:   x, u   y, u   x, v   y, v
Allowed substitution hints:   ph( x, y, v, u)
Proof of Theorem 2sb5ndVD
StepHypRef Expression
1 ax6e2ndeq 38775 . 2 |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
2 anabs5 851 . . . 4 |- ( ( 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 38768 . . . . . . . . 9 |- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( ( x = u /\ y = v ) /\ ph ) )
43exbii 1774 . . . . . . . 8 |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. y ( ( x = u /\ y = v ) /\ ph ) )
5 hbs1 2436 . . . . . . . . . . . . 13 |- ( [ u / x ] [ v / y ] ph -> A. x [ u / x ] [ v / y ] ph )
6 idn1 38790 . . . . . . . . . . . . . 14 |- (. A. x x = y ->. A. x x = y ).
7 axc11 2314 . . . . . . . . . . . . . 14 |- ( A. x x = y -> ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
86, 7e1a 38852 . . . . . . . . . . . . 13 |- (. A. x x = y ->. ( A. x [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
9 imim1 83 . . . . . . . . . . . . 13 |- ( ( [ 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 ) ) )
105, 8, 9e01 38916 . . . . . . . . . . . 12 |- (. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
1110in1 38787 . . . . . . . . . . 11 |- ( A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
12 hbs1 2436 . . . . . . . . . . . . . . 15 |- ( [ v / y ] ph -> A. y [ v / y ] ph )
1312sbt 2419 . . . . . . . . . . . . . 14 |- [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph )
14 sbi1 2392 . . . . . . . . . . . . . 14 |- ( [ u / x ] ( [ v / y ] ph -> A. y [ v / y ] ph ) -> ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph ) )
1513, 14e0a 38999 . . . . . . . . . . . . 13 |- ( [ u / x ] [ v / y ] ph -> [ u / x ] A. y [ v / y ] ph )
16 idn1 38790 . . . . . . . . . . . . . . 15 |- (. -. A. x x = y ->. -. A. x x = y ).
17 axc11n 2307 . . . . . . . . . . . . . . . 16 |- ( A. y y = x -> A. x x = y )
1817con3i 150 . . . . . . . . . . . . . . 15 |- ( -. A. x x = y -> -. A. y y = x )
1916, 18e1a 38852 . . . . . . . . . . . . . 14 |- (. -. A. x x = y ->. -. A. y y = x ).
20 sbal2 2461 . . . . . . . . . . . . . 14 |- ( -. A. y y = x -> ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) )
2119, 20e1a 38852 . . . . . . . . . . . . 13 |- (. -. A. x x = y ->. ( [ u / x ] A. y [ v / y ] ph <-> A. y [ u / x ] [ v / y ] ph ) ).
22 imbi2 338 . . . . . . . . . . . . . 14 |- ( ( [ 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 ) ) )
2322biimpcd 239 . . . . . . . . . . . . 13 |- ( ( [ 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 ) ) )
2415, 21, 23e01 38916 . . . . . . . . . . . 12 |- (. -. A. x x = y ->. ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) ).
2524in1 38787 . . . . . . . . . . 11 |- ( -. A. x x = y -> ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph ) )
2611, 25pm2.61i 176 . . . . . . . . . 10 |- ( [ u / x ] [ v / y ] ph -> A. y [ u / x ] [ v / y ] ph )
2726nf5i 2024 . . . . . . . . 9 |- F/ y [ u / x ] [ v / y ] ph
282719.41 2103 . . . . . . . 8 |- ( E. y ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
294, 28bitr3i 266 . . . . . . 7 |- ( E. y ( ( x = u /\ y = v ) /\ ph ) <-> ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
3029exbii 1774 . . . . . 6 |- ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) <-> E. x ( E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) )
315nf5i 2024 . . . . . . 7 |- F/ x [ u / x ] [ v / y ] ph
323119.41 2103 . . . . . 6 |- ( 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 ) )
3330, 32bitr2i 265 . . . . 5 |- ( ( E. x E. y ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
3433anbi2i 730 . . . 4 |- ( ( 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 ) ) )
352, 34bitr3i 266 . . 3 |- ( ( 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 668 . . 3 |- ( ( 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 ) ) ) )
3735, 36mpbir 221 . 2 |- ( E. x E. y ( x = u /\ y = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
381, 37sylbi 207 1 |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   [wsb 1880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ne 2795  df-v 3202  df-vd1 38786
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator