# 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 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({x}={y}\to \left({z}\in {w}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {z}\in {w}\right)\right)\right)$

### Proof

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