Metamath Proof Explorer

Theorem ralrnmpo

Description: A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypotheses rngop.1 ⊢F=x∈A,y∈B⟼C
ralrnmpo.2 ⊢z=C→φ↔ψ
Assertion ralrnmpo ⊢∀x∈A∀y∈BC∈V→∀z∈ran⁡Fφ↔∀x∈A∀y∈Bψ

Proof

Step Hyp Ref Expression
1 rngop.1 ⊢F=x∈A,y∈B⟼C
2 ralrnmpo.2 ⊢z=C→φ↔ψ
3 1 rnmpo ⊢ran⁡F=w|∃x∈A∃y∈Bw=C
4 3 raleqi ⊢∀z∈ran⁡Fφ↔∀z∈w|∃x∈A∃y∈Bw=Cφ
5 eqeq1 ⊢w=z→w=C↔z=C
6 5 2rexbidv ⊢w=z→∃x∈A∃y∈Bw=C↔∃x∈A∃y∈Bz=C
7 6 ralab ⊢∀z∈w|∃x∈A∃y∈Bw=Cφ↔∀z∃x∈A∃y∈Bz=C→φ
8 ralcom4 ⊢∀x∈A∀z∃y∈Bz=C→φ↔∀z∀x∈A∃y∈Bz=C→φ
9 r19.23v ⊢∀x∈A∃y∈Bz=C→φ↔∃x∈A∃y∈Bz=C→φ
10 9 albii ⊢∀z∀x∈A∃y∈Bz=C→φ↔∀z∃x∈A∃y∈Bz=C→φ
11 8 10 bitr2i ⊢∀z∃x∈A∃y∈Bz=C→φ↔∀x∈A∀z∃y∈Bz=C→φ
12 4 7 11 3bitri ⊢∀z∈ran⁡Fφ↔∀x∈A∀z∃y∈Bz=C→φ
13 ralcom4 ⊢∀y∈B∀zz=C→φ↔∀z∀y∈Bz=C→φ
14 r19.23v ⊢∀y∈Bz=C→φ↔∃y∈Bz=C→φ
15 14 albii ⊢∀z∀y∈Bz=C→φ↔∀z∃y∈Bz=C→φ
16 13 15 bitri ⊢∀y∈B∀zz=C→φ↔∀z∃y∈Bz=C→φ
17 nfv ⊢Ⅎzψ
18 17 2 ceqsalg ⊢C∈V→∀zz=C→φ↔ψ
19 18 ralimi ⊢∀y∈BC∈V→∀y∈B∀zz=C→φ↔ψ
20 ralbi ⊢∀y∈B∀zz=C→φ↔ψ→∀y∈B∀zz=C→φ↔∀y∈Bψ
21 19 20 syl ⊢∀y∈BC∈V→∀y∈B∀zz=C→φ↔∀y∈Bψ
22 16 21 bitr3id ⊢∀y∈BC∈V→∀z∃y∈Bz=C→φ↔∀y∈Bψ
23 22 ralimi ⊢∀x∈A∀y∈BC∈V→∀x∈A∀z∃y∈Bz=C→φ↔∀y∈Bψ
24 ralbi ⊢∀x∈A∀z∃y∈Bz=C→φ↔∀y∈Bψ→∀x∈A∀z∃y∈Bz=C→φ↔∀x∈A∀y∈Bψ
25 23 24 syl ⊢∀x∈A∀y∈BC∈V→∀x∈A∀z∃y∈Bz=C→φ↔∀x∈A∀y∈Bψ
26 12 25 bitrid ⊢∀x∈A∀y∈BC∈V→∀z∈ran⁡Fφ↔∀x∈A∀y∈Bψ