This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax12el

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

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

Proof

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