Theorem bj-rep 37805

Description: Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep 5236 (in the form of axrep6 5245). (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 3079	. . . 4 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 ↔ ∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑))
2		eumo 2605	. . . . . . 7 ⊢ (∃!𝑧𝜑 → ∃*𝑧𝜑)
3	2	imim2i 17	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
4		moanimv 2646	. . . . . 6 ⊢ (∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 → ∃*𝑧𝜑))
5	3, 4	sylibr 237	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
6	5	alimi 1844	. . . 4 ⊢ (∀𝑦(𝑦 ∈ 𝑥 → ∃!𝑧𝜑) → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
7	1, 6	sylbi 220	. . 3 ⊢ (∀𝑦 ∈ 𝑥 ∃!𝑧𝜑 → ∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑))
8		axrep6 5245	. . . 4 ⊢ (∀𝑦∃*𝑧(𝑦 ∈ 𝑥 ∧ 𝜑) → ∃𝑡∀𝑧(𝑧 ∈ 𝑡 ↔ ∃𝑦 ∈ 𝑥 (𝑦 ∈ 𝑥 ∧ 𝜑)))
9		rexanid 3113	. . . . . . 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 2564  ∃!weu 2595  ∀wral 3078  ∃wrex 3088

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 1943  ax-6 2000  ax-7 2041  ax-rep 5236

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2566  df-eu 2596  df-ral 3079  df-rex 3089

This theorem is used by: (None)