Metamath Proof Explorer

Theorem axsepg2

Description: A generalization of ax-sep in which y and z need not be distinct. See also axsepg which instead allows z to occur in ph . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BTernaryTau, 3-Aug-2025) (New usage is discouraged.)

Ref Expression
Assertion axsepg2 ⊢ ∃ 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-nul ⊢ ∃ y ∀ x ¬ x ∈ y
23 id ⊢ ¬ x ∈ y → ¬ x ∈ y
24 23 bianfd ⊢ ¬ x ∈ y → x ∈ y ↔ x ∈ y ∧ φ
25 24 alimi ⊢ ∀ x ¬ x ∈ y → ∀ x x ∈ y ↔ x ∈ y ∧ φ
26 22 25 eximii ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ y ∧ φ
27 8 9 14 20 21 26 dvelimexcasei ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ