Theorem replem

Description: A lemma for variants of the axiom of replacement: if we can form the set of images of the functional relation, then we can also form a set containing all its images. The converse requires the axiom of separation. (Contributed by BJ, 5-Apr-2026)

	Ref	Expression
Assertion	replem	⊢ ( ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 ∧ ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) ) → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		biimpr	⊢ ( ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) → ( ∃ 𝑥 ∈ 𝑧 𝜑 → 𝑦 ∈ 𝑤 ) )
2		r19.23v	⊢ ( ∀ 𝑥 ∈ 𝑧 ( 𝜑 → 𝑦 ∈ 𝑤 ) ↔ ( ∃ 𝑥 ∈ 𝑧 𝜑 → 𝑦 ∈ 𝑤 ) )
3	2	biimpri	⊢ ( ( ∃ 𝑥 ∈ 𝑧 𝜑 → 𝑦 ∈ 𝑤 ) → ∀ 𝑥 ∈ 𝑧 ( 𝜑 → 𝑦 ∈ 𝑤 ) )
4		ancr	⊢ ( ( 𝜑 → 𝑦 ∈ 𝑤 ) → ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) )
5	4	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑧 ( 𝜑 → 𝑦 ∈ 𝑤 ) → ∀ 𝑥 ∈ 𝑧 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) )
6	1 3 5	3syl	⊢ ( ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) → ∀ 𝑥 ∈ 𝑧 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) )
7	6	alimi	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) → ∀ 𝑦 ∀ 𝑥 ∈ 𝑧 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) )
8		ralcom4	⊢ ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) ↔ ∀ 𝑦 ∀ 𝑥 ∈ 𝑧 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) )
9	8	biimpri	⊢ ( ∀ 𝑦 ∀ 𝑥 ∈ 𝑧 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) → ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) )
10		exim	⊢ ( ∀ 𝑦 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) )
11		df-rex	⊢ ( ∃ 𝑦 ∈ 𝑤 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) )
12	10 11	imbitrrdi	⊢ ( ∀ 𝑦 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 ) )
13	12	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( 𝜑 → ( 𝑦 ∈ 𝑤 ∧ 𝜑 ) ) → ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 ) )
14	7 9 13	3syl	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) → ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 ) )
15		pm2.27	⊢ ( ∃ 𝑦 𝜑 → ( ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 ) → ∃ 𝑦 ∈ 𝑤 𝜑 ) )
16	15	ral2imi	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 → ( ∀ 𝑥 ∈ 𝑧 ( ∃ 𝑦 𝜑 → ∃ 𝑦 ∈ 𝑤 𝜑 ) → ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 ) )
17	14 16	syl5	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 → ( ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) → ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 ) )
18	17	eximdv	⊢ ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 → ( ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 ) )
19	18	imp	⊢ ( ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 ∧ ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) ) → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )