Theorem bj-rep

Description: Version of the axiom of replacement requiring the functional relation in the axiom to be a (total) function from ax-rep (in the form of axrep6 ). (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.) (New usage is discouraded.)

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

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑦 ∈ 𝑥 ∃! 𝑧 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃! 𝑧 𝜑 ) )
2		eumo	⊢ ( ∃! 𝑧 𝜑 → ∃* 𝑧 𝜑 )
3	2	imim2i	⊢ ( ( 𝑦 ∈ 𝑥 → ∃! 𝑧 𝜑 ) → ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) )
4		moanimv	⊢ ( ∃* 𝑧 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) )
5	3 4	sylibr	⊢ ( ( 𝑦 ∈ 𝑥 → ∃! 𝑧 𝜑 ) → ∃* 𝑧 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
6	5	alimi	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃! 𝑧 𝜑 ) → ∀ 𝑦 ∃* 𝑧 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
7	1 6	sylbi	⊢ ( ∀ 𝑦 ∈ 𝑥 ∃! 𝑧 𝜑 → ∀ 𝑦 ∃* 𝑧 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) )
8		axrep6	⊢ ( ∀ 𝑦 ∃* 𝑧 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ) )
9		rexanid	⊢ ( ∃ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑦 ∈ 𝑥 𝜑 )
10	9	bibi2i	⊢ ( ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) )
11	10	albii	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) )
12	11	exbii	⊢ ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) )
13	8 12	sylib	⊢ ( ∀ 𝑦 ∃* 𝑧 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) )
14	7 13	syl	⊢ ( ∀ 𝑦 ∈ 𝑥 ∃! 𝑧 𝜑 → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) )
15	14	ax-gen	⊢ ∀ 𝑥 ( ∀ 𝑦 ∈ 𝑥 ∃! 𝑧 𝜑 → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) )