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 ⊢ ∀ y y = z → ∀ x φ ↔ x = y ↔ ∀ x φ ↔ x = z
5 4 drex1 ⊢ ∀ y y = z → ∃ y ∀ x φ ↔ x = y ↔ ∃ z ∀ x φ ↔ x = z
6 hbnae ⊢ ¬ ∀ y y = z → ∀ y ¬ ∀ y y = z
7 hbnae ⊢ ¬ ∀ y y = z → ∀ z ¬ ∀ y y = z
8 6 7 alrimih ⊢ ¬ ∀ y y = z → ∀ y ∀ z ¬ ∀ y y = 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 ⊢ ¬ ∀ z z = y → ¬ ∀ x φ ↔ x = y → ∀ z ¬ ∀ x φ ↔ x = y
15 14 naecoms ⊢ ¬ ∀ y y = 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 ⊢ ¬ ∀ y y = z → ¬ ∀ x φ ↔ x = z → ∀ y ¬ ∀ x φ ↔ x = z
22 3 notbid ⊢ y = z → ¬ ∀ x φ ↔ x = y ↔ ¬ ∀ x φ ↔ x = z
23 22 a1i ⊢ ¬ ∀ y y = z → y = z → ¬ ∀ x φ ↔ x = y ↔ ¬ ∀ x φ ↔ x = z
24 15 21 23 cbv2h ⊢ ∀ y ∀ z ¬ ∀ y y = z → ∀ y ¬ ∀ x φ ↔ x = y ↔ ∀ z ¬ ∀ x φ ↔ x = z
25 8 24 syl ⊢ ¬ ∀ y y = z → ∀ y ¬ ∀ x φ ↔ x = y ↔ ∀ z ¬ ∀ x φ ↔ x = z
26 25 notbid ⊢ ¬ ∀ y y = 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 ⊢ ¬ ∀ y y = z → ∃ y ∀ x φ ↔ x = y ↔ ∃ z ∀ x φ ↔ x = z
30 5 29 pm2.61i ⊢ ∃ y ∀ x φ ↔ x = y ↔ ∃ z ∀ x φ ↔ x = z