Theorem axsepgfromrep 5234

Description: A more general version axsepg 5237 of the axiom scheme of separation ax-sep 5236 derived from the axiom scheme of replacement ax-rep 5217 (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 2142 to ax-13 2393. (Revised by SN, 25-Sep-2023.) Use ax-sep 5236 instead (or axsepg 5237 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 5226	. . 3 ⊢ (∀𝑤∃*𝑥(𝑤 = 𝑥 ∧ 𝜑) → ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)))
2		euequ 2614	. . . . 5 ⊢ ∃!𝑥 𝑥 = 𝑤
3	2	eumoi 2596	. . . 4 ⊢ ∃*𝑥 𝑥 = 𝑤
4		equcomi 2027	. . . . . 6 ⊢ (𝑤 = 𝑥 → 𝑥 = 𝑤)
5	4	adantr 483	. . . . 5 ⊢ ((𝑤 = 𝑥 ∧ 𝜑) → 𝑥 = 𝑤)
6	5	moimi 2562	. . . 4 ⊢ (∃*𝑥 𝑥 = 𝑤 → ∃*𝑥(𝑤 = 𝑥 ∧ 𝜑))
7	3, 6	ax-mp 5	. . 3 ⊢ ∃*𝑥(𝑤 = 𝑥 ∧ 𝜑)
8	1, 7	mpg 1807	. 2 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑))
9		df-rex 3077	. . . . . 6 ⊢ (∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
10		an12 653	. . . . . . 7 ⊢ ((𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
11	10	exbii 1858	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ ∃𝑤(𝑤 ∈ 𝑧 ∧ (𝑤 = 𝑥 ∧ 𝜑)))
12		elequ1 2139	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
13	12	anbi1d 639	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑤 ∈ 𝑧 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
14	13	equsexvw 2015	. . . . . 6 ⊢ (∃𝑤(𝑤 = 𝑥 ∧ (𝑤 ∈ 𝑧 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
15	9, 11, 14	3bitr2i 301	. . . . 5 ⊢ (∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑) ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
16	15	bibi2i 339	. . . 4 ⊢ ((𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
17	16	albii 1829	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
18	17	exbii 1858	. 2 ⊢ (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑧 (𝑤 = 𝑥 ∧ 𝜑)) ↔ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
19	8, 18	mpbi 232	1 ⊢ ∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∀wal 1548  ∃wex 1789  ∃*wmo 2554  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-rep 5217

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-mo 2556  df-eu 2586  df-rex 3077

This theorem is referenced by:  axsep  5235