# Metamath Proof Explorer

## Theorem axrepndlem2

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

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

### Proof

Step Hyp Ref Expression
1 axrepndlem1 ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \exists {w}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)\right)\right)$
2 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
3 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}$
4 2 3 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)$
5 nfnae ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
6 nfnae ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}$
7 5 6 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)$
8 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
9 nfnae ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}$
10 8 9 nfan ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)$
11 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }$
12 11 a1i ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }$
13 nfcvf ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
14 13 adantl ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
15 nfcvf ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
16 15 adantr ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
17 14 16 nfeqd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}={y}$
18 12 17 nfimd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)$
19 10 18 nfald ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)$
20 7 19 nfexd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)$
21 nfcvd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{w}$
22 14 21 nfeld ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {w}$
23 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)$
24 21 16 nfeld ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}\in {y}$
25 7 12 nfald ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }$
26 24 25 nfand ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)$
27 23 26 nfexd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)$
28 22 27 nfbid ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)\right)$
29 10 28 nfald ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)\right)$
30 20 29 nfimd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)\right)\right)$
31 nfcvd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{w}$
32 nfcvf2 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{x}$
33 32 adantr ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{x}$
34 31 33 nfeqd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{w}={x}$
35 7 34 nfan1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)$
36 nfcvd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{w}$
37 nfcvf2 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{x}$
38 37 adantl ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}{x}$
39 36 38 nfeqd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}{w}={x}$
40 10 39 nfan1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)$
41 sbequ12r ${⊢}{w}={x}\to \left(\left[{w}/{x}\right]{\phi }↔{\phi }\right)$
42 41 imbi1d ${⊢}{w}={x}\to \left(\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)↔\left({\phi }\to {z}={y}\right)\right)$
43 42 adantl ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)↔\left({\phi }\to {z}={y}\right)\right)$
44 40 43 albid ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={y}\right)\right)$
45 35 44 exbid ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={y}\right)\right)$
46 elequ2 ${⊢}{w}={x}\to \left({z}\in {w}↔{z}\in {x}\right)$
47 46 adantl ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left({z}\in {w}↔{z}\in {x}\right)$
48 elequ1 ${⊢}{w}={x}\to \left({w}\in {y}↔{x}\in {y}\right)$
49 48 adantl ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left({w}\in {y}↔{x}\in {y}\right)$
50 41 adantl ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\left[{w}/{x}\right]{\phi }↔{\phi }\right)$
51 35 50 albid ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
52 49 51 anbi12d ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)↔\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
53 52 ex ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left({w}={x}\to \left(\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)↔\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)$
54 4 26 53 cbvexd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
55 54 adantr ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
56 47 55 bibi12d ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\left({z}\in {w}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)\right)↔\left({z}\in {x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)$
57 40 56 albid ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)$
58 45 57 imbi12d ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge {w}={x}\right)\to \left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)\right)\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)\right)$
59 58 ex ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left({w}={x}\to \left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)\right)\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)\right)\right)$
60 4 30 59 cbvexd ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left(\exists {w}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{w}/{x}\right]{\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {w}↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left[{w}/{x}\right]{\phi }\right)\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)\right)$
61 1 60 syl5ib ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to \left(¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)\right)$
62 61 imp ${⊢}\left(\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\wedge ¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\right)$