Metamath Proof Explorer

Theorem axsepg2ALT

Description: Alternate proof of axsepg2 , derived directly from ax-sep with no additional set theory axioms. (Contributed by BTernaryTau, 3-Aug-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axsepg2ALT ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ x ¬ ∀ y y = z
2 nfvd ⊢ ¬ ∀ y y = z → Ⅎ y x ∈ w
3 nfcvf ⊢ ¬ ∀ y y = z → Ⅎ _ y z
4 3 nfcrd ⊢ ¬ ∀ y y = z → Ⅎ y x ∈ z
5 nfvd ⊢ ¬ ∀ y y = z → Ⅎ y φ
6 4 5 nfand ⊢ ¬ ∀ y y = z → Ⅎ y x ∈ z ∧ φ
7 2 6 nfbid ⊢ ¬ ∀ y y = z → Ⅎ y x ∈ w ↔ x ∈ z ∧ φ
8 1 7 nfald ⊢ ¬ ∀ y y = z → Ⅎ y ∀ x x ∈ w ↔ x ∈ z ∧ φ
9 nfvd ⊢ ¬ ∀ y y = z → Ⅎ w ∀ x x ∈ y ↔ x ∈ z ∧ φ
10 elequ2 ⊢ w = y → x ∈ w ↔ x ∈ y
11 10 bibi1d ⊢ w = y → x ∈ w ↔ x ∈ z ∧ φ ↔ x ∈ y ↔ x ∈ z ∧ φ
12 11 biimpd ⊢ w = y → x ∈ w ↔ x ∈ z ∧ φ → x ∈ y ↔ x ∈ z ∧ φ
13 12 alimdv ⊢ w = y → ∀ x x ∈ w ↔ x ∈ z ∧ φ → ∀ x x ∈ y ↔ x ∈ z ∧ φ
14 13 a1i ⊢ ¬ ∀ y y = z → w = y → ∀ x x ∈ w ↔ x ∈ z ∧ φ → ∀ x x ∈ y ↔ x ∈ z ∧ φ
15 elequ2 ⊢ y = z → x ∈ y ↔ x ∈ z
16 15 anbi1d ⊢ y = z → x ∈ y ∧ φ ↔ x ∈ z ∧ φ
17 16 bibi2d ⊢ y = z → x ∈ y ↔ x ∈ y ∧ φ ↔ x ∈ y ↔ x ∈ z ∧ φ
18 17 biimpd ⊢ y = z → x ∈ y ↔ x ∈ y ∧ φ → x ∈ y ↔ x ∈ z ∧ φ
19 18 alimdv ⊢ y = z → ∀ x x ∈ y ↔ x ∈ y ∧ φ → ∀ x x ∈ y ↔ x ∈ z ∧ φ
20 19 sps ⊢ ∀ y y = z → ∀ x x ∈ y ↔ x ∈ y ∧ φ → ∀ x x ∈ y ↔ x ∈ z ∧ φ
21 ax-sep ⊢ ∃ w ∀ x x ∈ w ↔ x ∈ z ∧ φ
22 ax-sep ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ v ∧ ⊥
23 fal ⊢ ¬ ⊥
24 23 intnan ⊢ ¬ x ∈ v ∧ ⊥
25 biimp ⊢ x ∈ y ↔ x ∈ v ∧ ⊥ → x ∈ y → x ∈ v ∧ ⊥
26 24 25 mtoi ⊢ x ∈ y ↔ x ∈ v ∧ ⊥ → ¬ x ∈ y
27 26 bianfd ⊢ x ∈ y ↔ x ∈ v ∧ ⊥ → x ∈ y ↔ x ∈ y ∧ φ
28 27 alimi ⊢ ∀ x x ∈ y ↔ x ∈ v ∧ ⊥ → ∀ x x ∈ y ↔ x ∈ y ∧ φ
29 22 28 eximii ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ y ∧ φ
30 8 9 14 20 21 29 dvelimexcasei ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ