Metamath Proof Explorer

Theorem axpowndlem4

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 4-Jan-2002) (Proof shortened by Mario Carneiro, 10-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion axpowndlem4 ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\to \left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(¬{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)\right)$

Proof

Step Hyp Ref Expression
1 axpowndlem3 ${⊢}¬{x}={w}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)$
2 1 ax-gen ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left(¬{x}={w}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)\right)$
3 nfnae ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}$
4 nfnae ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}$
5 3 4 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)$
6 nfcvf ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{x}$
7 6 adantr ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{x}$
8 nfcvd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{w}$
9 7 8 nfeqd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}={w}$
10 9 nfnd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬{x}={w}$
11 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}$
12 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}$
13 11 12 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)$
14 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)$
15 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}$
16 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}$
17 15 16 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)$
18 7 8 nfeld ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {w}$
19 17 18 nfexd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}$
20 nfcvf ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{z}$
21 20 adantl ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{z}$
22 7 21 nfeld ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {z}$
23 14 22 nfald ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}$
24 19 23 nfimd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)$
25 13 24 nfald ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)$
26 8 7 nfeld ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{w}\in {x}$
27 25 26 nfimd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)$
28 14 27 nfald ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)$
29 13 28 nfexd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)$
30 10 29 nfimd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(¬{x}={w}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)\right)$
31 equequ2 ${⊢}{w}={y}\to \left({x}={w}↔{x}={y}\right)$
32 31 notbid ${⊢}{w}={y}\to \left(¬{x}={w}↔¬{x}={y}\right)$
33 32 adantl ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left(¬{x}={w}↔¬{x}={y}\right)$
34 nfcvd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{w}$
35 nfcvf2 ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
36 35 adantr ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
37 34 36 nfeqd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}={y}$
38 13 37 nfan1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)$
39 nfcvd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{w}$
40 nfcvf2 ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{y}$
41 40 adantl ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{y}$
42 39 41 nfeqd ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}{w}={y}$
43 17 42 nfan1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)$
44 elequ2 ${⊢}{w}={y}\to \left({x}\in {w}↔{x}\in {y}\right)$
45 44 adantl ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left({x}\in {w}↔{x}\in {y}\right)$
46 43 45 exbid ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}↔\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\right)$
47 biidd ${⊢}{w}={y}\to \left({x}\in {z}↔{x}\in {z}\right)$
48 47 a1i ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \left({w}={y}\to \left({x}\in {z}↔{x}\in {z}\right)\right)$
49 5 22 48 cbvald ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}↔\forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)$
50 49 adantr ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}↔\forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)$
51 46 50 imbi12d ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left(\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)↔\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\right)$
52 38 51 albid ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\right)$
53 elequ1 ${⊢}{w}={y}\to \left({w}\in {x}↔{y}\in {x}\right)$
54 53 adantl ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left({w}\in {x}↔{y}\in {x}\right)$
55 52 54 imbi12d ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left(\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)$
56 55 ex ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \left({w}={y}\to \left(\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)\right)$
57 5 27 56 cbvald ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)$
58 13 57 exbid ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)$
59 58 adantr ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)$
60 33 59 imbi12d ${⊢}\left(\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\wedge {w}={y}\right)\to \left(\left(¬{x}={w}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)\right)↔\left(¬{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)\right)$
61 60 ex ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \left({w}={y}\to \left(\left(¬{x}={w}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)\right)↔\left(¬{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)\right)\right)$
62 5 30 61 cbvald ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\left(¬{x}={w}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {w}\to \forall {w}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {w}\in {x}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(¬{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)\right)$
63 2 62 mpbii ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(¬{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)$
64 63 19.21bi ${⊢}\left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \left(¬{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)$
65 64 ex ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={x}\to \left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(¬{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\exists {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to \forall {y}\phantom{\rule{.4em}{0ex}}{x}\in {z}\right)\to {y}\in {x}\right)\right)\right)$