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 ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) )

Proof

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