Theorem axsepgfromrep 5221

Description: A more general version axsepg 5224 of the axiom scheme of separation ax-sep 5223 derived from the axiom scheme of replacement ax-rep 5209 (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 2116 to ax-13 2372. (Revised by SN, 25-Sep-2023.) Use ax-sep 5223 instead (or axsepg 5224 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 5216	. . 3 ⊢ (∀𝑤∃*𝑥(𝑤 = 𝑥 ∧ 𝜑) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)))
2		euequ 2597	. . . . 5 ⊢ ∃!𝑥 𝑥 = 𝑤
3	2	eumoi 2579	. . . 4 ⊢ ∃*𝑥 𝑥 = 𝑤
4		equcomi 2020	. . . . . 6 ⊢ (𝑤 = 𝑥 → 𝑥 = 𝑤)
5	4	adantr 481	. . . . 5 ⊢ ((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑤)
6	5	moimi 2545	. . . 4 ⊢ (∃*𝑥 𝑥 = 𝑤 → ∃*𝑥(𝑤 = 𝑥 ∧ 𝜑))
7	3, 6	ax-mp 5	. . 3 ⊢ ∃*𝑥(𝑤 = 𝑥 ∧ 𝜑)
8	1, 7	mpg 1800	. 2 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑))
9		df-rex 3070	. . . . . 6 ⊢ (∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
10		an12 642	. . . . . . 7 ⊢ ((𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
11	10	exbii 1850	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
12		elequ1 2113	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
13	12	anbi1d 630	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
14	13	equsexvw 2008	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
15	9, 11, 14	3bitr2i 299	. . . . 5 ⊢ (∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
16	15	bibi2i 338	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
17	16	albii 1822	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
18	17	exbii 1850	. 2 ⊢ (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
19	8, 18	mpbi 229	1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∀wal 1537  ∃wex 1782  ∃*wmo 2538  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-rep 5209

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-mo 2540  df-eu 2569  df-rex 3070

This theorem is referenced by:  axsep  5222