Theorem bj-rep 37368

Description: Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep 5201 (in the form of axrep6 5210). (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 3050	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑))
2		eumo 2577	. . . . . . 7 ⊢ (∃!𝑧𝜑 → ∃*𝑧𝜑)
3	2	imim2i 16	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
4		moanimv 2618	. . . . . 6 ⊢ (∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
5	3, 4	sylibr 234	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
6	5	alimi 1813	. . . 4 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
7	1, 6	sylbi 217	. . 3 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
8		axrep6 5210	. . . 4 ⊢ (∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)))
9		rexanid 3084	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑦 ∈ 𝑥 𝜑)
10	9	bibi2i 337	. . . . . 6 ⊢ ((𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
11	10	albii 1821	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
12	11	exbii 1850	. . . 4 ⊢ (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
13	8, 12	sylib 218	. . 3 ⊢ (∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
14	7, 13	syl 17	. 2 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
15	14	ax-gen 1797	1 ⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540  ∃wex 1781  ∃*wmo 2536  ∃!weu 2567  ∀wral 3049  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-rep 5201

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2538  df-eu 2568  df-ral 3050  df-rex 3060

This theorem is referenced by: (None)