Metamath Proof Explorer

Theorem axsepgfromrep

Description: A more general version axsepg of the axiom scheme of separation ax-sep derived from the axiom scheme of replacement ax-rep (and first-order logic). The extra generality consists in the absence of a disjoint variable condition on z , ph (that is, variable z may occur in formula ph ). See linked statements for more information. (Contributed by NM, 11-Sep-2006) Remove dependencies on ax-9 to ax-13 . (Revised by SN, 25-Sep-2023) Use ax-sep instead (or axsepg if the extra generality is needed). (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axrep6 ⊢ ∀ w ∃* x w = x ∧ φ → ∃ y ∀ x x ∈ y ↔ ∃ w ∈ z w = x ∧ φ
2 euequ ⊢ ∃! x x = w
3 2 eumoi ⊢ ∃* x x = w
4 equcomi ⊢ w = x → x = w
5 4 adantr ⊢ w = x ∧ φ → x = w
6 5 moimi ⊢ ∃* x x = w → ∃* x w = x ∧ φ
7 3 6 ax-mp ⊢ ∃* x w = x ∧ φ
8 1 7 mpg ⊢ ∃ y ∀ x x ∈ y ↔ ∃ w ∈ z w = x ∧ φ
9 df-rex ⊢ ∃ w ∈ z w = x ∧ φ ↔ ∃ w w ∈ z ∧ w = x ∧ φ
10 an12 ⊢ w = x ∧ w ∈ z ∧ φ ↔ w ∈ z ∧ w = x ∧ φ
11 10 exbii ⊢ ∃ w w = x ∧ w ∈ z ∧ φ ↔ ∃ w w ∈ z ∧ w = x ∧ φ
12 elequ1 ⊢ w = x → w ∈ z ↔ x ∈ z
13 12 anbi1d ⊢ w = x → w ∈ z ∧ φ ↔ x ∈ z ∧ φ
14 13 equsexvw ⊢ ∃ w w = x ∧ w ∈ z ∧ φ ↔ x ∈ z ∧ φ
15 9 11 14 3bitr2i ⊢ ∃ w ∈ z w = x ∧ φ ↔ x ∈ z ∧ φ
16 15 bibi2i ⊢ x ∈ y ↔ ∃ w ∈ z w = x ∧ φ ↔ x ∈ y ↔ x ∈ z ∧ φ
17 16 albii ⊢ ∀ x x ∈ y ↔ ∃ w ∈ z w = x ∧ φ ↔ ∀ x x ∈ y ↔ x ∈ z ∧ φ
18 17 exbii ⊢ ∃ y ∀ x x ∈ y ↔ ∃ w ∈ z w = x ∧ φ ↔ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ
19 8 18 mpbi ⊢ ∃ y ∀ x x ∈ y ↔ x ∈ z ∧ φ