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 ⊢ ∀ x ∈ z ∃ y φ ∧ ∃ w ∀ y y ∈ w ↔ ∃ x ∈ z φ → ∃ w ∀ x ∈ z ∃ y ∈ w φ

Proof

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