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

Theorem ax6e2ndeqVD 37216
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 36847) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 36831 is ax6e2ndeqVD 37216 without virtual deductions and was automatically derived from ax6e2ndeqVD 37216. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. u  =/=  v  ->.  u  =/=  v ).
2::  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  (  x  =  u  /\  y  =  v ) ).
3:2:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =  u ).
4:1,3:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  v ).
5:2:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  y  =  v ).
6:4,5:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  y ).
7::  |-  ( A. x x  =  y  ->  x  =  y )
8:7:  |-  ( -.  x  =  y  ->  -.  A. x x  =  y )
9::  |-  ( -.  x  =  y  <->  x  =/=  y )
10:8,9:  |-  ( x  =/=  y  ->  -.  A. x x  =  y )
11:6,10:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  -.  A. x x  =  y ).
12:11:  |-  (. u  =/=  v  ->.  ( ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
13:12:  |-  (. u  =/=  v  ->.  A. x ( ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
14:13:  |-  (. u  =/=  v  ->.  ( E. x ( x  =  u  /\  y  =  v )  ->  E. x -.  A. x x  =  y ) ).
15::  |-  ( -.  A. x x  =  y  ->  A. x -.  A. x x  =  y  )
19:15:  |-  ( E. x -.  A. x x  =  y  <->  -.  A. x x  =  y )
20:14,19:  |-  (. u  =/=  v  ->.  ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
21:20:  |-  (. u  =/=  v  ->.  A. y ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
22:21:  |-  (. u  =/=  v  ->.  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y -.  A. x x  =  y ) ).
23::  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  <->  E.  y E. x ( x  =  u  /\  y  =  v ) )
24:22,23:  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y -.  A. x x  =  y ) ).
25::  |-  ( -.  A. x x  =  y  ->  A. y -.  A. x x  =  y  )
26:25:  |-  ( E. y -.  A. x x  =  y  ->  E. y A. y -.  A. x x  =  y )
260::  |-  ( A. y -.  A. x x  =  y  ->  A. y A. y -.  A. x x  =  y )
27:260:  |-  ( E. y A. y -.  A. x x  =  y  <->  A. y -.  A. x x  =  y )
270:26,27:  |-  ( E. y -.  A. x x  =  y  ->  A. y -.  A. x  x  =  y )
28::  |-  ( A. y -.  A. x x  =  y  ->  -.  A. x x  =  y  )
29:270,28:  |-  ( E. y -.  A. x x  =  y  ->  -.  A. x x  =  y  )
30:24,29:  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
31:30:  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) ).
32:31:  |-  ( u  =/=  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) )
33::  |-  (. u  =  v  ->.  u  =  v ).
34:33:  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  u  =  v ) ).
35:34:  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) ).
36:35:  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) )
37::  |-  ( u  =  v  \/  u  =/=  v )
38:32,36,37:  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  (  -.  A. x x  =  y  \/  u  =  v ) )
39::  |-  ( A. x x  =  y  ->  ( u  =  v  ->  E. x E. y  ( x  =  u  /\  y  =  v ) ) )
40::  |-  ( -.  A. x x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
41:40:  |-  ( -.  A. x x  =  y  ->  ( u  =  v  ->  E. x E.  y ( x  =  u  /\  y  =  v ) ) )
42::  |-  ( A. x x  =  y  \/  -.  A. x x  =  y )
43:39,41,42:  |-  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v  ) )
44:40,43:  |-  ( ( -.  A. x x  =  y  \/  u  =  v )  ->  E. x  E. y ( x  =  u  /\  y  =  v ) )
qed:38,44:  |-  ( ( -.  A. x x  =  y  \/  u  =  v )  <->  E. x  E. y ( x  =  u  /\  y  =  v ) )
Assertion
Ref Expression
ax6e2ndeqVD  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  <->  E. x E. y ( x  =  u  /\  y  =  v ) )
Distinct variable groups:    x, u    y, u    x, v    y,
v

Proof of Theorem ax6e2ndeqVD
StepHypRef Expression
1 ax6e2nd 36832 . . 3  |-  ( -. 
A. x  x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
2 ax6e2eq 36831 . . . 4  |-  ( A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y
( x  =  u  /\  y  =  v ) ) )
31a1d 26 . . . 4  |-  ( -. 
A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) )
4 exmid 416 . . . 4  |-  ( A. x  x  =  y  \/  -.  A. x  x  =  y )
5 jao 514 . . . 4  |-  ( ( A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) )  ->  ( ( -. 
A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) )  ->  ( ( A. x  x  =  y  \/  -.  A. x  x  =  y )  -> 
( u  =  v  ->  E. x E. y
( x  =  u  /\  y  =  v ) ) ) ) )
62, 3, 4, 5e000 37064 . . 3  |-  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
71, 6jaoi 380 . 2  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  ->  E. x E. y ( x  =  u  /\  y  =  v )
)
8 idn1 36852 . . . . . . . . . . . . . . . 16  |-  (. u  =/=  v  ->.  u  =/=  v ).
9 idn2 36900 . . . . . . . . . . . . . . . . 17  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  ( x  =  u  /\  y  =  v ) ).
10 simpl 458 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
119, 10e2 36918 . . . . . . . . . . . . . . . 16  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =  u ).
12 neeq1 2657 . . . . . . . . . . . . . . . . 17  |-  ( x  =  u  ->  (
x  =/=  v  <->  u  =/=  v ) )
1312biimprcd 228 . . . . . . . . . . . . . . . 16  |-  ( u  =/=  v  ->  (
x  =  u  ->  x  =/=  v ) )
148, 11, 13e12 37021 . . . . . . . . . . . . . . 15  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  v ).
15 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
169, 15e2 36918 . . . . . . . . . . . . . . 15  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  y  =  v ).
17 neeq2 2658 . . . . . . . . . . . . . . . 16  |-  ( y  =  v  ->  (
x  =/=  y  <->  x  =/=  v ) )
1817biimprcd 228 . . . . . . . . . . . . . . 15  |-  ( x  =/=  v  ->  (
y  =  v  ->  x  =/=  y ) )
1914, 16, 18e22 36958 . . . . . . . . . . . . . 14  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  y ).
20 df-ne 2595 . . . . . . . . . . . . . . . 16  |-  ( x  =/=  y  <->  -.  x  =  y )
2120bicomi 205 . . . . . . . . . . . . . . 15  |-  ( -.  x  =  y  <->  x  =/=  y )
22 sp 1914 . . . . . . . . . . . . . . . 16  |-  ( A. x  x  =  y  ->  x  =  y )
2322con3i 140 . . . . . . . . . . . . . . 15  |-  ( -.  x  =  y  ->  -.  A. x  x  =  y )
2421, 23sylbir 216 . . . . . . . . . . . . . 14  |-  ( x  =/=  y  ->  -.  A. x  x  =  y )
2519, 24e2 36918 . . . . . . . . . . . . 13  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  -.  A. x  x  =  y ).
2625in2 36892 . . . . . . . . . . . 12  |-  (. u  =/=  v  ->.  ( ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
2726gen11 36903 . . . . . . . . . . 11  |-  (. u  =/=  v  ->.  A. x ( ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
28 exim 1700 . . . . . . . . . . 11  |-  ( A. x ( ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y )  ->  ( E. x ( x  =  u  /\  y  =  v )  ->  E. x  -.  A. x  x  =  y ) )
2927, 28e1a 36914 . . . . . . . . . 10  |-  (. u  =/=  v  ->.  ( E. x
( x  =  u  /\  y  =  v )  ->  E. x  -.  A. x  x  =  y ) ).
30 nfnae 2118 . . . . . . . . . . 11  |-  F/ x  -.  A. x  x  =  y
313019.9 1947 . . . . . . . . . 10  |-  ( E. x  -.  A. x  x  =  y  <->  -.  A. x  x  =  y )
32 imbi2 325 . . . . . . . . . . 11  |-  ( ( E. x  -.  A. x  x  =  y  <->  -. 
A. x  x  =  y )  ->  (
( E. x ( x  =  u  /\  y  =  v )  ->  E. x  -.  A. x  x  =  y
)  <->  ( E. x
( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y )
) )
3332biimpcd 227 . . . . . . . . . 10  |-  ( ( E. x ( x  =  u  /\  y  =  v )  ->  E. x  -.  A. x  x  =  y )  ->  ( ( E. x  -.  A. x  x  =  y  <->  -.  A. x  x  =  y )  ->  ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ) )
3429, 31, 33e10 36981 . . . . . . . . 9  |-  (. u  =/=  v  ->.  ( E. x
( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
3534gen11 36903 . . . . . . . 8  |-  (. u  =/=  v  ->.  A. y ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
36 exim 1700 . . . . . . . 8  |-  ( A. y ( E. x
( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y )  ->  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) )
3735, 36e1a 36914 . . . . . . 7  |-  (. u  =/=  v  ->.  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) ).
38 excom 1903 . . . . . . 7  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  <->  E. y E. x ( x  =  u  /\  y  =  v )
)
39 imbi1 324 . . . . . . . 8  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  <->  E. y E. x
( x  =  u  /\  y  =  v ) )  ->  (
( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y )  <->  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y )
) )
4039biimprcd 228 . . . . . . 7  |-  ( ( E. y E. x
( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y )  ->  (
( E. x E. y ( x  =  u  /\  y  =  v )  <->  E. y E. x ( x  =  u  /\  y  =  v ) )  -> 
( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) ) )
4137, 38, 40e10 36981 . . . . . 6  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y ) ).
42 hbnae 2117 . . . . . . . . 9  |-  ( -. 
A. x  x  =  y  ->  A. y  -.  A. x  x  =  y )
4342eximi 1701 . . . . . . . 8  |-  ( E. y  -.  A. x  x  =  y  ->  E. y A. y  -. 
A. x  x  =  y )
44 nfa1 1956 . . . . . . . . 9  |-  F/ y A. y  -.  A. x  x  =  y
454419.9 1947 . . . . . . . 8  |-  ( E. y A. y  -. 
A. x  x  =  y  <->  A. y  -.  A. x  x  =  y
)
4643, 45sylib 199 . . . . . . 7  |-  ( E. y  -.  A. x  x  =  y  ->  A. y  -.  A. x  x  =  y )
47 sp 1914 . . . . . . 7  |-  ( A. y  -.  A. x  x  =  y  ->  -.  A. x  x  =  y )
4846, 47syl 17 . . . . . 6  |-  ( E. y  -.  A. x  x  =  y  ->  -. 
A. x  x  =  y )
49 imim1 79 . . . . . 6  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  ->  E. y  -.  A. x  x  =  y )  ->  (
( E. y  -. 
A. x  x  =  y  ->  -.  A. x  x  =  y )  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ) )
5041, 48, 49e10 36981 . . . . 5  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y ) ).
51 orc 386 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  ( -.  A. x  x  =  y  \/  u  =  v ) )
5251imim2i 16 . . . . 5  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  ->  -.  A. x  x  =  y )  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) )
5350, 52e1a 36914 . . . 4  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) ).
5453in1 36849 . . 3  |-  ( u  =/=  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )
55 idn1 36852 . . . . . 6  |-  (. u  =  v  ->.  u  =  v ).
56 ax-1 6 . . . . . 6  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  u  =  v ) )
5755, 56e1a 36914 . . . . 5  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  u  =  v ) ).
58 olc 385 . . . . . 6  |-  ( u  =  v  ->  ( -.  A. x  x  =  y  \/  u  =  v ) )
5958imim2i 16 . . . . 5  |-  ( ( E. x E. y
( x  =  u  /\  y  =  v )  ->  u  =  v )  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )
6057, 59e1a 36914 . . . 4  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) ).
6160in1 36849 . . 3  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )
62 exmidne 2604 . . 3  |-  ( u  =  v  \/  u  =/=  v )
63 jao 514 . . . 4  |-  ( ( u  =  v  -> 
( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) )  ->  ( ( u  =/=  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )  ->  (
( u  =  v  \/  u  =/=  v
)  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  -> 
( -.  A. x  x  =  y  \/  u  =  v )
) ) ) )
6463com12 32 . . 3  |-  ( ( u  =/=  v  -> 
( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v ) ) )  ->  ( ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
) )  ->  (
( u  =  v  \/  u  =/=  v
)  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  -> 
( -.  A. x  x  =  y  \/  u  =  v )
) ) ) )
6554, 61, 62, 64e000 37064 . 2  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x  x  =  y  \/  u  =  v )
)
667, 65impbii 190 1  |-  ( ( -.  A. x  x  =  y  \/  u  =  v )  <->  E. x E. y ( x  =  u  /\  y  =  v ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370   A.wal 1435    = wceq 1437   E.wex 1657    =/= wne 2593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-ne 2595  df-v 3018  df-vd1 36848  df-vd2 36856
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator