Metamath Proof Explorer

Theorem axsepg5

Description: A generalization of ax-sep that combines axsepg , axsepg2 , and axsepg3 into a single theorem scheme. Unlike ax-sep , this scheme lacks a distinct variable condition for ph and z , for x and z , and for y and z . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 24-May-2026) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfnae ⊢ Ⅎ 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 albidv ⊢ w = y → ∀ x x ∈ w ↔ x ∈ z ∧ φ ↔ ∀ x x ∈ y ↔ x ∈ z ∧ φ
13 12 biimpd ⊢ 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 nfae ⊢ Ⅎ x ∀ y y = z
16 elequ2 ⊢ y = z → x ∈ y ↔ x ∈ z
17 16 anbi1d ⊢ y = z → x ∈ y ∧ φ ↔ x ∈ z ∧ φ
18 17 bibi2d ⊢ y = z → x ∈ y ↔ x ∈ y ∧ φ ↔ x ∈ y ↔ x ∈ z ∧ φ
19 18 biimpd ⊢ y = z → x ∈ y ↔ x ∈ y ∧ φ → x ∈ y ↔ x ∈ z ∧ φ
20 19 sps ⊢ ∀ y y = z → x ∈ y ↔ x ∈ y ∧ φ → x ∈ y ↔ x ∈ z ∧ φ
21 15 20 alimd ⊢ ∀ y y = z → ∀ x x ∈ y ↔ x ∈ y ∧ φ → ∀ x x ∈ y ↔ x ∈ z ∧ φ
22 axsepg4 ⊢ ∃ w ∀ x x ∈ w ↔ x ∈ z ∧ φ
23 axsepg3 ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ y ∧ φ
24 8 9 14 21 22 23 dvelimexcasei ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ