Theorem axsepgfromrep 5216

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

Assertion

Ref	Expression
axsepgfromrep	⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Distinct variable groups:   𝑥,𝑦,𝑧   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑧)

Proof of Theorem axsepgfromrep

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axrep6 5212	. . 3 ⊢ (∀𝑤∃*𝑥(𝑤 = 𝑥 ∧ 𝜑) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)))
2		euequ 2597	. . . . 5 ⊢ ∃!𝑥 𝑥 = 𝑤
3	2	eumoi 2579	. . . 4 ⊢ ∃*𝑥 𝑥 = 𝑤
4		equcomi 2021	. . . . . 6 ⊢ (𝑤 = 𝑥 → 𝑥 = 𝑤)
5	4	adantr 480	. . . . 5 ⊢ ((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑤)
6	5	moimi 2545	. . . 4 ⊢ (∃*𝑥 𝑥 = 𝑤 → ∃*𝑥(𝑤 = 𝑥 ∧ 𝜑))
7	3, 6	ax-mp 5	. . 3 ⊢ ∃*𝑥(𝑤 = 𝑥 ∧ 𝜑)
8	1, 7	mpg 1801	. 2 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑))
9		df-rex 3069	. . . . . 6 ⊢ (∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
10		an12 641	. . . . . . 7 ⊢ ((𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
11	10	exbii 1851	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
12		elequ1 2115	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
13	12	anbi1d 629	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
14	13	equsexvw 2009	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
15	9, 11, 14	3bitr2i 298	. . . . 5 ⊢ (∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
16	15	bibi2i 337	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
17	16	albii 1823	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
18	17	exbii 1851	. 2 ⊢ (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
19	8, 18	mpbi 229	1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ wa 395  ∀wal 1537  ∃wex 1783  ∃*wmo 2538  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-rep 5205

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-mo 2540  df-eu 2569  df-rex 3069

This theorem is referenced by:  axsep  5217