This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 𝜑 ∧ ∃ 𝑤 ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ ∃ 𝑥 ∈ 𝑧 𝜑 ) ) → ∃ 𝑤 ∀ 𝑥 ∈ 𝑧 ∃ 𝑦 ∈ 𝑤 𝜑 )