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