Theorem bj-rep 38031

Description: Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep 5231 (in the form of axrep6 5239). (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 3077	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑))
2		eumo 2603	. . . . . . 7 ⊢ (∃!𝑧𝜑 → ∃*𝑧𝜑)
3	2	imim2i 17	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
4		moanimv 2644	. . . . . 6 ⊢ (∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
5	3, 4	sylibr 237	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
6	5	alimi 1843	. . . 4 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
7	1, 6	sylbi 220	. . 3 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
8		axrep6 5239	. . . 4 ⊢ (∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)))
9		rexanid 3111	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑦 ∈ 𝑥 𝜑)
10	9	bibi2i 340	. . . . . 6 ⊢ ((𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
11	10	albii 1851	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
12	11	exbii 1880	. . . 4 ⊢ (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
13	8, 12	sylib 221	. . 3 ⊢ (∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
14	7, 13	syl 18	. 2 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
15	14	ax-gen 1827	1 ⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  ∃wex 1811  ∃*wmo 2562  ∃!weu 2593  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-rep 5231

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2564  df-eu 2594  df-ral 3077  df-rex 3087

This theorem is used by: (None)