Metamath Proof Explorer

Theorem ax6e2eqVD

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. ax6e2eq is ax6e2eqVD without virtual deductions and was automatically derived from ax6e2eqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- (. A. x x = y ->. A. x x = y ).
2:: |- (. A. x x = y ,. x = u ->. x = u ).
3:1: |- (. A. x x = y ->. x = y ).
4:2,3: |- (. A. x x = y ,. x = u ->. y = u ).
5:2,4: |- (. A. x x = y ,. x = u ->. ( x = u /\ y = u ) ).
6:5: |- (. A. x x = y ->. ( x = u -> ( x = u /\ y = u ) ) ).
7:6: |- ( A. x x = y -> ( x = u -> ( x = u /\ y = u ) ) )
8:7: |- ( A. x A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
9:: |- ( A. x x = y <-> A. x A. x x = y )
10:8,9: |- ( A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
11:1,10: |- (. A. x x = y ->. A. x ( x = u -> ( x = u /\ y = u ) ) ).
12:11: |- (. A. x x = y ->. ( E. x x = u -> E. x ( x = u /\ y = u ) ) ).
13:: |- E. x x = u
14:13,12: |- (. A. x x = y ->. E. x ( x = u /\ y = u ) ).
140:14: |- ( A. x x = y -> E. x ( x = u /\ y = u ) )
141:140: |- ( A. x x = y -> A. x E. x ( x = u /\ y = u ) )
15:1,141: |- (. A. x x = y ->. A. x E. x ( x = u /\ y = u ) ).
16:1,15: |- (. A. x x = y ->. A. y E. x ( x = u /\ y = u ) ).
17:16: |- (. A. x x = y ->. E. y E. x ( x = u /\ y = u ) ).
18:17: |- (. A. x x = y ->. E. x E. y ( x = u /\ y = u ) ).
19:: |- (. u = v ->. u = v ).
20:: |- (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = u ) ).
21:20: |- (. u = v ,. ( x = u /\ y = u ) ->. y = u ).
22:19,21: |- (. u = v ,. ( x = u /\ y = u ) ->. y = v ).
23:20: |- (. u = v ,. ( x = u /\ y = u ) ->. x = u ).
24:22,23: |- (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = v ) ).
25:24: |- (. u = v ->. ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
26:25: |- (. u = v ->. A. y ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
27:26: |- (. u = v ->. ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
28:27: |- (. u = v ->. A. x ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
29:28: |- (. u = v ->. ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ).
30:29: |- ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) )
31:18,30: |- (. A. x x = y ->. ( u = v -> E. x E. y ( x = u /\ y = v ) ) ).
qed:31: |- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )

Ref Expression
Assertion ax6e2eqVD ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ∀ 𝑥 𝑥 = 𝑦    )
2 ax6ev ⊢ ∃ 𝑥 𝑥 = 𝑢
3 hba1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ∀ 𝑥 𝑥 = 𝑦 )
4 sp ⊢ ( ∀ 𝑥 ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 𝑥 = 𝑦 )
5 3 4 impbii ⊢ ( ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑥 ∀ 𝑥 𝑥 = 𝑦 )
6 idn2 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ,    𝑥 = 𝑢    ▶    𝑥 = 𝑢    )
7 sp ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
8 1 7 e1a ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    𝑥 = 𝑦    )
9 ax7 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑢 → 𝑦 = 𝑢 ) )
10 9 com12 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 = 𝑦 → 𝑦 = 𝑢 ) )
11 6 8 10 e21 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ,    𝑥 = 𝑢    ▶    𝑦 = 𝑢    )
12 pm3.2 ⊢ ( 𝑥 = 𝑢 → ( 𝑦 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
13 6 11 12 e22 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ,    𝑥 = 𝑢    ▶    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    )
14 13 in2 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ( 𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )    )
15 14 in1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
16 15 alimi ⊢ ( ∀ 𝑥 ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
17 5 16 sylbi ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
18 1 17 e1a ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ∀ 𝑥 ( 𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )    )
19 exim ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) → ( ∃ 𝑥 𝑥 = 𝑢 → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
20 18 19 e1a ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ( ∃ 𝑥 𝑥 = 𝑢 → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )    )
21 pm2.27 ⊢ ( ∃ 𝑥 𝑥 = 𝑢 → ( ( ∃ 𝑥 𝑥 = 𝑢 → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
22 2 20 21 e01 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    )
23 22 in1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
24 23 axc4i ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
25 1 24 e1a ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ∀ 𝑥 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    )
26 axc11 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∀ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) ) )
27 1 25 26 e11 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ∀ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    )
28 19.2 ⊢ ( ∀ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
29 27 28 e1a ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    )
30 excomim ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) )
31 29 30 e1a ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    )
32 idn1 ⊢ (    𝑢 = 𝑣    ▶    𝑢 = 𝑣    )
33 idn2 ⊢ (    𝑢 = 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    ▶    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    )
34 simpr ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → 𝑦 = 𝑢 )
35 33 34 e2 ⊢ (    𝑢 = 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    ▶    𝑦 = 𝑢    )
36 equtrr ⊢ ( 𝑢 = 𝑣 → ( 𝑦 = 𝑢 → 𝑦 = 𝑣 ) )
37 32 35 36 e12 ⊢ (    𝑢 = 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    ▶    𝑦 = 𝑣    )
38 simpl ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → 𝑥 = 𝑢 )
39 33 38 e2 ⊢ (    𝑢 = 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    ▶    𝑥 = 𝑢    )
40 pm3.21 ⊢ ( 𝑦 = 𝑣 → ( 𝑥 = 𝑢 → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
41 37 39 40 e22 ⊢ (    𝑢 = 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 )    ▶    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    )
42 41 in2 ⊢ (    𝑢 = 𝑣    ▶    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )    )
43 42 gen11 ⊢ (    𝑢 = 𝑣    ▶    ∀ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )    )
44 exim ⊢ ( ∀ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) → ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
45 43 44 e1a ⊢ (    𝑢 = 𝑣    ▶    ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )    )
46 45 gen11 ⊢ (    𝑢 = 𝑣    ▶    ∀ 𝑥 ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )    )
47 exim ⊢ ( ∀ 𝑥 ( ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
48 46 47 e1a ⊢ (    𝑢 = 𝑣    ▶    ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )    )
49 48 in1 ⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
50 pm2.04 ⊢ ( ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) ) )
51 50 com12 ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) ) → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) ) )
52 31 49 51 e10 ⊢ (    ∀ 𝑥 𝑥 = 𝑦    ▶    ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )    )
53 52 in1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )