Metamath Proof Explorer

Theorem ax6e2ndeqVD

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 ax6e2ndeqVD without virtual deductions and was automatically derived from ax6e2ndeqVD . (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 ) )

Ref Expression
Assertion ax6e2ndeqVD ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )

Proof

Step Hyp Ref Expression
1 ax6e2nd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
2 ax6e2eq ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
3 1 a1d ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
4 exmid ⊢ ( ∀ 𝑥 𝑥 = 𝑦 ∨ ¬ ∀ 𝑥 𝑥 = 𝑦 )
5 jao ⊢ ( ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) ) → ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) ) → ( ( ∀ 𝑥 𝑥 = 𝑦 ∨ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) ) ) )
6 2 3 4 5 e000 ⊢ ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
7 1 6 jaoi ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
8 idn1 ⊢ (    𝑢 ≠ 𝑣    ▶    𝑢 ≠ 𝑣    )
9 idn2 ⊢ (    𝑢 ≠ 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    ▶    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    )
10 simpl ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑥 = 𝑢 )
11 9 10 e2 ⊢ (    𝑢 ≠ 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    ▶    𝑥 = 𝑢    )
12 neeq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 ≠ 𝑣 ↔ 𝑢 ≠ 𝑣 ) )
13 12 biimprcd ⊢ ( 𝑢 ≠ 𝑣 → ( 𝑥 = 𝑢 → 𝑥 ≠ 𝑣 ) )
14 8 11 13 e12 ⊢ (    𝑢 ≠ 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    ▶    𝑥 ≠ 𝑣    )
15 simpr ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
16 9 15 e2 ⊢ (    𝑢 ≠ 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    ▶    𝑦 = 𝑣    )
17 neeq2 ⊢ ( 𝑦 = 𝑣 → ( 𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑣 ) )
18 17 biimprcd ⊢ ( 𝑥 ≠ 𝑣 → ( 𝑦 = 𝑣 → 𝑥 ≠ 𝑦 ) )
19 14 16 18 e22 ⊢ (    𝑢 ≠ 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    ▶    𝑥 ≠ 𝑦    )
20 df-ne ⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
21 20 bicomi ⊢ ( ¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦 )
22 sp ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
23 22 con3i ⊢ ( ¬ 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
24 21 23 sylbir ⊢ ( 𝑥 ≠ 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
25 19 24 e2 ⊢ (    𝑢 ≠ 𝑣    ,    ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    ▶    ¬ ∀ 𝑥 𝑥 = 𝑦    )
26 25 in2 ⊢ (    𝑢 ≠ 𝑣    ▶    ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 )    )
27 26 gen11 ⊢ (    𝑢 ≠ 𝑣    ▶    ∀ 𝑥 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 )    )
28 exim ⊢ ( ∀ 𝑥 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
29 27 28 e1a ⊢ (    𝑢 ≠ 𝑣    ▶    ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 )    )
30 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
31 30 19.9 ⊢ ( ∃ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 )
32 imbi2 ⊢ ( ( ∃ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 ) ↔ ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 ) ) )
33 32 biimpcd ⊢ ( ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ( ∃ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 ) ) )
34 29 31 33 e10 ⊢ (    𝑢 ≠ 𝑣    ▶    ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 )    )
35 34 gen11 ⊢ (    𝑢 ≠ 𝑣    ▶    ∀ 𝑦 ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 )    )
36 exim ⊢ ( ∀ 𝑦 ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
37 35 36 e1a ⊢ (    𝑢 ≠ 𝑣    ▶    ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 )    )
38 excom ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
39 imbi1 ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) → ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ) ↔ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ) ) )
40 39 biimprcd ⊢ ( ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ) ) )
41 37 38 40 e10 ⊢ (    𝑢 ≠ 𝑣    ▶    ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 )    )
42 hbnae ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 )
43 42 eximi ⊢ ( ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 )
44 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
45 44 19.9 ⊢ ( ∃ 𝑦 ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ↔ ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 )
46 43 45 sylib ⊢ ( ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 )
47 sp ⊢ ( ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
48 46 47 syl ⊢ ( ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
49 imim1 ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ( ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 ) ) )
50 41 48 49 e10 ⊢ (    𝑢 ≠ 𝑣    ▶    ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 )    )
51 orc ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )
52 51 imim2i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) )
53 50 52 e1a ⊢ (    𝑢 ≠ 𝑣    ▶    ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )    )
54 53 in1 ⊢ ( 𝑢 ≠ 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) )
55 idn1 ⊢ (    𝑢 = 𝑣    ▶    𝑢 = 𝑣    )
56 ax-1 ⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑢 = 𝑣 ) )
57 55 56 e1a ⊢ (    𝑢 = 𝑣    ▶    ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑢 = 𝑣 )    )
58 olc ⊢ ( 𝑢 = 𝑣 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )
59 58 imim2i ⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑢 = 𝑣 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) )
60 57 59 e1a ⊢ (    𝑢 = 𝑣    ▶    ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )    )
61 60 in1 ⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) )
62 exmidne ⊢ ( 𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣 )
63 jao ⊢ ( ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) ) → ( ( 𝑢 ≠ 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) ) → ( ( 𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) ) ) )
64 63 com12 ⊢ ( ( 𝑢 ≠ 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) ) → ( ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) ) → ( ( 𝑢 = 𝑣 ∨ 𝑢 ≠ 𝑣 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) ) ) )
65 54 61 62 64 e000 ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )
66 7 65 impbii ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )