Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax6e2ndALT Structured version   Unicode version

Theorem ax6e2ndALT 33873
Description: If at least two sets exist (dtru 4647) , then the same is true expressed in an alternate form similar to the form of ax6e 2003. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndVD 33851. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax6e2ndALT  |-  ( -. 
A. x  x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
Distinct variable groups:    x, u    y, u    x, v

Proof of Theorem ax6e2ndALT
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 vex 3112 . . . . . . 7  |-  u  e. 
_V
2 ax6e 2003 . . . . . . 7  |-  E. y 
y  =  v
31, 2pm3.2i 455 . . . . . 6  |-  ( u  e.  _V  /\  E. y  y  =  v
)
4 19.42v 1776 . . . . . . 7  |-  ( E. y ( u  e. 
_V  /\  y  =  v )  <->  ( u  e.  _V  /\  E. y 
y  =  v ) )
54biimpri 206 . . . . . 6  |-  ( ( u  e.  _V  /\  E. y  y  =  v )  ->  E. y
( u  e.  _V  /\  y  =  v ) )
63, 5ax-mp 5 . . . . 5  |-  E. y
( u  e.  _V  /\  y  =  v )
7 isset 3113 . . . . . . 7  |-  ( u  e.  _V  <->  E. x  x  =  u )
87anbi1i 695 . . . . . 6  |-  ( ( u  e.  _V  /\  y  =  v )  <->  ( E. x  x  =  u  /\  y  =  v ) )
98exbii 1668 . . . . 5  |-  ( E. y ( u  e. 
_V  /\  y  =  v )  <->  E. y
( E. x  x  =  u  /\  y  =  v ) )
106, 9mpbi 208 . . . 4  |-  E. y
( E. x  x  =  u  /\  y  =  v )
11 id 22 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  -.  A. x  x  =  y )
12 hbnae 2058 . . . . . . 7  |-  ( -. 
A. x  x  =  y  ->  A. y  -.  A. x  x  =  y )
13 hbn1 1839 . . . . . . . . . . . 12  |-  ( -. 
A. x  x  =  y  ->  A. x  -.  A. x  x  =  y )
14 ax-5 1705 . . . . . . . . . . . . . . . 16  |-  ( z  =  v  ->  A. x  z  =  v )
15 ax-5 1705 . . . . . . . . . . . . . . . 16  |-  ( y  =  v  ->  A. z 
y  =  v )
16 id 22 . . . . . . . . . . . . . . . . 17  |-  ( z  =  y  ->  z  =  y )
17 equequ1 1799 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  y  ->  (
z  =  v  <->  y  =  v ) )
1817a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( z  =  y  -> 
z  =  y )  ->  ( z  =  y  ->  ( z  =  v  <->  y  =  v ) ) )
1916, 18ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  (
z  =  v  <->  y  =  v ) )
2014, 15, 19dvelimh 2079 . . . . . . . . . . . . . . 15  |-  ( -. 
A. x  x  =  y  ->  ( y  =  v  ->  A. x  y  =  v )
)
2111, 20syl 16 . . . . . . . . . . . . . 14  |-  ( -. 
A. x  x  =  y  ->  ( y  =  v  ->  A. x  y  =  v )
)
2221idiALT 33361 . . . . . . . . . . . . 13  |-  ( -. 
A. x  x  =  y  ->  ( y  =  v  ->  A. x  y  =  v )
)
2322alimi 1634 . . . . . . . . . . . 12  |-  ( A. x  -.  A. x  x  =  y  ->  A. x
( y  =  v  ->  A. x  y  =  v ) )
2413, 23syl 16 . . . . . . . . . . 11  |-  ( -. 
A. x  x  =  y  ->  A. x
( y  =  v  ->  A. x  y  =  v ) )
2511, 24syl 16 . . . . . . . . . 10  |-  ( -. 
A. x  x  =  y  ->  A. x
( y  =  v  ->  A. x  y  =  v ) )
26 19.41rg 33466 . . . . . . . . . 10  |-  ( A. x ( y  =  v  ->  A. x  y  =  v )  ->  ( ( E. x  x  =  u  /\  y  =  v )  ->  E. x ( x  =  u  /\  y  =  v ) ) )
2725, 26syl 16 . . . . . . . . 9  |-  ( -. 
A. x  x  =  y  ->  ( ( E. x  x  =  u  /\  y  =  v )  ->  E. x
( x  =  u  /\  y  =  v ) ) )
2827idiALT 33361 . . . . . . . 8  |-  ( -. 
A. x  x  =  y  ->  ( ( E. x  x  =  u  /\  y  =  v )  ->  E. x
( x  =  u  /\  y  =  v ) ) )
2928alimi 1634 . . . . . . 7  |-  ( A. y  -.  A. x  x  =  y  ->  A. y
( ( E. x  x  =  u  /\  y  =  v )  ->  E. x ( x  =  u  /\  y  =  v ) ) )
3012, 29syl 16 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  A. y
( ( E. x  x  =  u  /\  y  =  v )  ->  E. x ( x  =  u  /\  y  =  v ) ) )
3111, 30syl 16 . . . . 5  |-  ( -. 
A. x  x  =  y  ->  A. y
( ( E. x  x  =  u  /\  y  =  v )  ->  E. x ( x  =  u  /\  y  =  v ) ) )
32 exim 1655 . . . . 5  |-  ( A. y ( ( E. x  x  =  u  /\  y  =  v )  ->  E. x
( x  =  u  /\  y  =  v ) )  ->  ( E. y ( E. x  x  =  u  /\  y  =  v )  ->  E. y E. x
( x  =  u  /\  y  =  v ) ) )
3331, 32syl 16 . . . 4  |-  ( -. 
A. x  x  =  y  ->  ( E. y ( E. x  x  =  u  /\  y  =  v )  ->  E. y E. x
( x  =  u  /\  y  =  v ) ) )
34 pm3.35 587 . . . 4  |-  ( ( E. y ( E. x  x  =  u  /\  y  =  v )  /\  ( E. y ( E. x  x  =  u  /\  y  =  v )  ->  E. y E. x
( x  =  u  /\  y  =  v ) ) )  ->  E. y E. x ( x  =  u  /\  y  =  v )
)
3510, 33, 34sylancr 663 . . 3  |-  ( -. 
A. x  x  =  y  ->  E. y E. x ( x  =  u  /\  y  =  v ) )
36 excomim 1851 . . 3  |-  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. x E. y
( x  =  u  /\  y  =  v ) )
3735, 36syl 16 . 2  |-  ( -. 
A. x  x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
3837idiALT 33361 1  |-  ( -. 
A. x  x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1393    = wceq 1395   E.wex 1613    e. wcel 1819   _Vcvv 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator