# Metamath Proof Explorer

## Theorem eujustALT

Description: Alternate proof of eujust illustrating the use of dvelim . (Contributed by NM, 11-Mar-2010) (Proof modification is discouraged.) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 equequ2 ${⊢}{y}={z}\to \left({x}={y}↔{x}={z}\right)$
2 1 bibi2d ${⊢}{y}={z}\to \left(\left({\phi }↔{x}={y}\right)↔\left({\phi }↔{x}={z}\right)\right)$
3 2 albidv ${⊢}{y}={z}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
4 3 sps ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
5 4 drex1 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
6 hbnae ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}$
7 hbnae ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}$
8 6 7 alrimih ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}$
9 ax-5 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={w}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={w}\right)$
10 equequ2 ${⊢}{w}={y}\to \left({x}={w}↔{x}={y}\right)$
11 10 bibi2d ${⊢}{w}={y}\to \left(\left({\phi }↔{x}={w}\right)↔\left({\phi }↔{x}={y}\right)\right)$
12 11 albidv ${⊢}{w}={y}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={w}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)$
13 12 notbid ${⊢}{w}={y}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={w}\right)↔¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)$
14 9 13 dvelim ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)$
15 14 naecoms ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)$
16 ax-5 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={w}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={w}\right)$
17 equequ2 ${⊢}{w}={z}\to \left({x}={w}↔{x}={z}\right)$
18 17 bibi2d ${⊢}{w}={z}\to \left(\left({\phi }↔{x}={w}\right)↔\left({\phi }↔{x}={z}\right)\right)$
19 18 albidv ${⊢}{w}={z}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={w}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
20 19 notbid ${⊢}{w}={z}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={w}\right)↔¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
21 16 20 dvelim ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
22 3 notbid ${⊢}{y}={z}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
23 22 a1i ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left({y}={z}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)\right)$
24 15 21 23 cbv2h ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
25 8 24 syl ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
26 25 notbid ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(¬\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔¬\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
27 df-ex ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔¬\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$
28 df-ex ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)↔¬\forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)$
29 26 27 28 3bitr4g ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)\right)$
30 5 29 pm2.61i ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={z}\right)$