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∀xx∈y↔x∈z∧φ

Proof

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