Metamath Proof Explorer

Theorem rnmposs

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017)

Ref Expression
Hypothesis rnmposs.1 ⊢F=x∈A,y∈B⟼C
Assertion rnmposs ⊢∀x∈A∀y∈BC∈D→ran⁡F⊆D

Proof

Step Hyp Ref Expression
1 rnmposs.1 ⊢F=x∈A,y∈B⟼C
2 1 rnmpo ⊢ran⁡F=z|∃x∈A∃y∈Bz=C
3 2 eqabri ⊢z∈ran⁡F↔∃x∈A∃y∈Bz=C
4 2r19.29 ⊢∀x∈A∀y∈BC∈D∧∃x∈A∃y∈Bz=C→∃x∈A∃y∈BC∈D∧z=C
5 eleq1 ⊢z=C→z∈D↔C∈D
6 5 biimparc ⊢C∈D∧z=C→z∈D
7 6 a1i ⊢x∈A∧y∈B→C∈D∧z=C→z∈D
8 7 rexlimivv ⊢∃x∈A∃y∈BC∈D∧z=C→z∈D
9 4 8 syl ⊢∀x∈A∀y∈BC∈D∧∃x∈A∃y∈Bz=C→z∈D
10 9 ex ⊢∀x∈A∀y∈BC∈D→∃x∈A∃y∈Bz=C→z∈D
11 3 10 biimtrid ⊢∀x∈A∀y∈BC∈D→z∈ran⁡F→z∈D
12 11 ssrdv ⊢∀x∈A∀y∈BC∈D→ran⁡F⊆D