Metamath Proof Explorer

Theorem ax12eq

Description: Basis step for constructing a substitution instance of ax-c15 without using ax-c15 . Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax12eq ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 19.26 ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) ↔ ( ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) )
2 equid ⊢ 𝑥 = 𝑥
3 2 a1i ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑥 )
4 3 ax-gen ⊢ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑥 )
5 4 a1i ⊢ ( 𝑥 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑥 ) )
6 equequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑥 ↔ 𝑧 = 𝑥 ) )
7 equequ2 ⊢ ( 𝑥 = 𝑤 → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑤 ) )
8 6 7 sylan9bb ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( 𝑥 = 𝑥 ↔ 𝑧 = 𝑤 ) )
9 8 sps-o ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( 𝑥 = 𝑥 ↔ 𝑧 = 𝑤 ) )
10 nfa1-o ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 )
11 9 imbi2d ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( ( 𝑥 = 𝑦 → 𝑥 = 𝑥 ) ↔ ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
12 10 11 albid ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
13 9 12 imbi12d ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( ( 𝑥 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑥 ) ) ↔ ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
14 13 adantr ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( ( 𝑥 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑥 ) ) ↔ ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
15 5 14 mpbii ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
16 15 exp32 ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) ) )
17 1 16 sylbir ⊢ ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) ) )
18 equequ1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑤 ↔ 𝑦 = 𝑤 ) )
19 18 ad2antll ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑥 = 𝑤 ↔ 𝑦 = 𝑤 ) )
20 axc9 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑦 = 𝑤 → ∀ 𝑥 𝑦 = 𝑤 ) ) )
21 20 impcom ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑦 = 𝑤 → ∀ 𝑥 𝑦 = 𝑤 ) )
22 21 adantrr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑦 = 𝑤 → ∀ 𝑥 𝑦 = 𝑤 ) )
23 equtrr ⊢ ( 𝑦 = 𝑤 → ( 𝑥 = 𝑦 → 𝑥 = 𝑤 ) )
24 23 alimi ⊢ ( ∀ 𝑥 𝑦 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑤 ) )
25 22 24 syl6 ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑦 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑤 ) ) )
26 19 25 sylbid ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑥 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑤 ) ) )
27 26 adantll ⊢ ( ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑥 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑤 ) ) )
28 equequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑤 ↔ 𝑧 = 𝑤 ) )
29 28 sps-o ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 = 𝑤 ↔ 𝑧 = 𝑤 ) )
30 29 imbi2d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( 𝑥 = 𝑦 → 𝑥 = 𝑤 ) ↔ ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
31 30 dral2-o ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑤 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
32 29 31 imbi12d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( 𝑥 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑤 ) ) ↔ ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
33 32 ad2antrr ⊢ ( ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( ( 𝑥 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑤 ) ) ↔ ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
34 27 33 mpbid ⊢ ( ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
35 34 exp32 ⊢ ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) ) )
36 equequ2 ⊢ ( 𝑥 = 𝑦 → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) )
37 36 ad2antll ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑦 ) )
38 axc9 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) ) )
39 38 imp ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )
40 39 adantrr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )
41 36 biimprcd ⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → 𝑧 = 𝑥 ) )
42 41 alimi ⊢ ( ∀ 𝑥 𝑧 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑥 ) )
43 40 42 syl6 ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑥 ) ) )
44 37 43 sylbid ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑥 ) ) )
45 44 adantlr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑥 ) ) )
46 7 sps-o ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( 𝑧 = 𝑥 ↔ 𝑧 = 𝑤 ) )
47 46 imbi2d ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ( 𝑥 = 𝑦 → 𝑧 = 𝑥 ) ↔ ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
48 47 dral2-o ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
49 46 48 imbi12d ⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ( 𝑧 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑥 ) ) ↔ ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
50 49 ad2antlr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( ( 𝑧 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑥 ) ) ↔ ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
51 45 50 mpbid ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
52 51 exp32 ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) ) )
53 ax6ev ⊢ ∃ 𝑢 𝑢 = 𝑤
54 ax6ev ⊢ ∃ 𝑣 𝑣 = 𝑧
55 ax-1 ⊢ ( 𝑣 = 𝑢 → ( 𝑥 = 𝑦 → 𝑣 = 𝑢 ) )
56 55 alrimiv ⊢ ( 𝑣 = 𝑢 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑣 = 𝑢 ) )
57 equequ1 ⊢ ( 𝑣 = 𝑧 → ( 𝑣 = 𝑢 ↔ 𝑧 = 𝑢 ) )
58 equequ2 ⊢ ( 𝑢 = 𝑤 → ( 𝑧 = 𝑢 ↔ 𝑧 = 𝑤 ) )
59 57 58 sylan9bb ⊢ ( ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( 𝑣 = 𝑢 ↔ 𝑧 = 𝑤 ) )
60 59 adantl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( 𝑣 = 𝑢 ↔ 𝑧 = 𝑤 ) )
61 dveeq2-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( 𝑣 = 𝑧 → ∀ 𝑥 𝑣 = 𝑧 ) )
62 dveeq2-o ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑢 = 𝑤 → ∀ 𝑥 𝑢 = 𝑤 ) )
63 61 62 im2anan9 ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( ∀ 𝑥 𝑣 = 𝑧 ∧ ∀ 𝑥 𝑢 = 𝑤 ) ) )
64 63 imp ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( ∀ 𝑥 𝑣 = 𝑧 ∧ ∀ 𝑥 𝑢 = 𝑤 ) )
65 19.26 ⊢ ( ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ↔ ( ∀ 𝑥 𝑣 = 𝑧 ∧ ∀ 𝑥 𝑢 = 𝑤 ) )
66 64 65 sylibr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) )
67 nfa1-o ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 )
68 59 sps-o ⊢ ( ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( 𝑣 = 𝑢 ↔ 𝑧 = 𝑤 ) )
69 68 imbi2d ⊢ ( ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( ( 𝑥 = 𝑦 → 𝑣 = 𝑢 ) ↔ ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
70 67 69 albid ⊢ ( ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑣 = 𝑢 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
71 66 70 syl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑣 = 𝑢 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
72 60 71 imbi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( ( 𝑣 = 𝑢 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑣 = 𝑢 ) ) ↔ ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
73 56 72 mpbii ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
74 73 exp32 ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( 𝑣 = 𝑧 → ( 𝑢 = 𝑤 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) ) )
75 74 exlimdv ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ∃ 𝑣 𝑣 = 𝑧 → ( 𝑢 = 𝑤 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) ) )
76 54 75 mpi ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( 𝑢 = 𝑤 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
77 76 exlimdv ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ∃ 𝑢 𝑢 = 𝑤 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
78 53 77 mpi ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) )
79 78 a1d ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( 𝑥 = 𝑦 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )
80 79 a1d ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) ) )
81 17 35 52 80 4cases ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 = 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 = 𝑤 ) ) ) )