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 ⊢∃y∀xφ↔x=y↔∃z∀xφ↔x=z

Proof

Step Hyp Ref Expression
1 equequ2 ⊢y=z→x=y↔x=z
2 1 bibi2d ⊢y=z→φ↔x=y↔φ↔x=z
3 2 albidv ⊢y=z→∀xφ↔x=y↔∀xφ↔x=z
4 3 sps ⊢∀yy=z→∀xφ↔x=y↔∀xφ↔x=z
5 4 drex1 ⊢∀yy=z→∃y∀xφ↔x=y↔∃z∀xφ↔x=z
6 hbnae ⊢¬∀yy=z→∀y¬∀yy=z
7 hbnae ⊢¬∀yy=z→∀z¬∀yy=z
8 6 7 alrimih ⊢¬∀yy=z→∀y∀z¬∀yy=z
9 ax-5 ⊢¬∀xφ↔x=w→∀z¬∀xφ↔x=w
10 equequ2 ⊢w=y→x=w↔x=y
11 10 bibi2d ⊢w=y→φ↔x=w↔φ↔x=y
12 11 albidv ⊢w=y→∀xφ↔x=w↔∀xφ↔x=y
13 12 notbid ⊢w=y→¬∀xφ↔x=w↔¬∀xφ↔x=y
14 9 13 dvelim ⊢¬∀zz=y→¬∀xφ↔x=y→∀z¬∀xφ↔x=y
15 14 naecoms ⊢¬∀yy=z→¬∀xφ↔x=y→∀z¬∀xφ↔x=y
16 ax-5 ⊢¬∀xφ↔x=w→∀y¬∀xφ↔x=w
17 equequ2 ⊢w=z→x=w↔x=z
18 17 bibi2d ⊢w=z→φ↔x=w↔φ↔x=z
19 18 albidv ⊢w=z→∀xφ↔x=w↔∀xφ↔x=z
20 19 notbid ⊢w=z→¬∀xφ↔x=w↔¬∀xφ↔x=z
21 16 20 dvelim ⊢¬∀yy=z→¬∀xφ↔x=z→∀y¬∀xφ↔x=z
22 3 notbid ⊢y=z→¬∀xφ↔x=y↔¬∀xφ↔x=z
23 22 a1i ⊢¬∀yy=z→y=z→¬∀xφ↔x=y↔¬∀xφ↔x=z
24 15 21 23 cbv2h ⊢∀y∀z¬∀yy=z→∀y¬∀xφ↔x=y↔∀z¬∀xφ↔x=z
25 8 24 syl ⊢¬∀yy=z→∀y¬∀xφ↔x=y↔∀z¬∀xφ↔x=z
26 25 notbid ⊢¬∀yy=z→¬∀y¬∀xφ↔x=y↔¬∀z¬∀xφ↔x=z
27 df-ex ⊢∃y∀xφ↔x=y↔¬∀y¬∀xφ↔x=y
28 df-ex ⊢∃z∀xφ↔x=z↔¬∀z¬∀xφ↔x=z
29 26 27 28 3bitr4g ⊢¬∀yy=z→∃y∀xφ↔x=y↔∃z∀xφ↔x=z
30 5 29 pm2.61i ⊢∃y∀xφ↔x=y↔∃z∀xφ↔x=z