Theorem axsepgfromrep 5294

Description: A more general version axsepg 5297 of the axiom scheme of separation ax-sep 5296 derived from the axiom scheme of replacement ax-rep 5279 (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 2377. (Revised by SN, 25-Sep-2023.) Use ax-sep 5296 instead (or axsepg 5297 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 5288	. . 3 ⊢ (∀𝑤∃*𝑥(𝑤 = 𝑥 ∧ 𝜑) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)))
2		euequ 2597	. . . . 5 ⊢ ∃!𝑥 𝑥 = 𝑤
3	2	eumoi 2579	. . . 4 ⊢ ∃*𝑥 𝑥 = 𝑤
4		equcomi 2016	. . . . . 6 ⊢ (𝑤 = 𝑥 → 𝑥 = 𝑤)
5	4	adantr 480	. . . . 5 ⊢ ((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑤)
6	5	moimi 2545	. . . 4 ⊢ (∃*𝑥 𝑥 = 𝑤 → ∃*𝑥(𝑤 = 𝑥 ∧ 𝜑))
7	3, 6	ax-mp 5	. . 3 ⊢ ∃*𝑥(𝑤 = 𝑥 ∧ 𝜑)
8	1, 7	mpg 1797	. 2 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑))
9		df-rex 3071	. . . . . 6 ⊢ (∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
10		an12 645	. . . . . . 7 ⊢ ((𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
11	10	exbii 1848	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
12		elequ1 2115	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
13	12	anbi1d 631	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
14	13	equsexvw 2004	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
15	9, 11, 14	3bitr2i 299	. . . . 5 ⊢ (∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
16	15	bibi2i 337	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
17	16	albii 1819	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
18	17	exbii 1848	. 2 ⊢ (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
19	8, 18	mpbi 230	1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779  ∃*wmo 2538  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-rep 5279

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-eu 2569  df-rex 3071

This theorem is referenced by:  axsep  5295