Theorem bj-rep 38180

Description: Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep 5235 (in the form of axrep6 5243). (Contributed by BJ, 14-Mar-2026.) The proof proves the statement without the DV condition on 𝑥, 𝜑, but the DV condition is added to this statement to show that this weaker version is sufficient. (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
bj-rep	⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))

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

Allowed substitution hints:   𝜑(𝑦, 𝑧)

Proof of Theorem bj-rep

Step	Hyp	Ref	Expression
1		df-ral 3081	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑))
2		eumo 2606	. . . . . . 7 ⊢ (∃!𝑧𝜑 → ∃*𝑧𝜑)
3	2	imim2i 17	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
4		moanimv 2647	. . . . . 6 ⊢ (∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
5	3, 4	sylibr 237	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
6	5	alimi 1844	. . . 4 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
7	1, 6	sylbi 220	. . 3 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
8		axrep6 5243	. . . 4 ⊢ (∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)))
9		rexanid 3115	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑦 ∈ 𝑥 𝜑)
10	9	bibi2i 340	. . . . . 6 ⊢ ((𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
11	10	albii 1852	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
12	11	exbii 1881	. . . 4 ⊢ (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
13	8, 12	sylib 221	. . 3 ⊢ (∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
14	7, 13	syl 18	. 2 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
15	14	ax-gen 1828	1 ⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812  ∃*wmo 2565  ∃!weu 2596  ∀wral 3080  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-rep 5235

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2567  df-eu 2597  df-ral 3081  df-rex 3091

This theorem is used by: (None)