Theorem bj-rep 37563

Description: Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep 5228 (in the form of axrep6 5237). (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 3078	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑))
2		eumo 2606	. . . . . . 7 ⊢ (∃!𝑧𝜑 → ∃*𝑧𝜑)
3	2	imim2i 16	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
4		moanimv 2647	. . . . . 6 ⊢ (∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
5	3, 4	sylibr 236	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
6	5	alimi 1832	. . . 4 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
7	1, 6	sylbi 219	. . 3 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
8		axrep6 5237	. . . 4 ⊢ (∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)))
9		rexanid 3112	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑) ↔ ∃𝑦 ∈ 𝑥 𝜑)
10	9	bibi2i 339	. . . . . 6 ⊢ ((𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ (𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
11	10	albii 1840	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ ∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
12	11	exbii 1869	. . . 4 ⊢ (∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)) ↔ ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
13	8, 12	sylib 220	. . 3 ⊢ (∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
14	7, 13	syl 17	. 2 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))
15	14	ax-gen 1816	1 ⊢ ∀𝑥(∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1559  ∃wex 1800  ∃*wmo 2565  ∃!weu 2596  ∀wral 3077  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-rep 5228

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-mo 2567  df-eu 2597  df-ral 3078  df-rex 3088

This theorem is referenced by: (None)