This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ( 𝑥 ∈ 𝑧 ∧ 𝜑 ) )

Proof

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