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

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 e. A , y e. B |-> C )
ralrnmpo.2 
|- ( z = C -> ( ph <-> ps ) )
Assertion ralrnmpo 
|- ( A. x e. A A. y e. B C e. V -> ( A. z e. ran F ph <-> A. x e. A A. y e. B ps ) )

Proof

Step Hyp Ref Expression
1 rngop.1 
 |-  F = ( x e. A , y e. B |-> C )
2 ralrnmpo.2 
 |-  ( z = C -> ( ph <-> ps ) )
3 1 rnmpo 
 |-  ran F = { w | E. x e. A E. y e. B w = C }
4 3 raleqi 
 |-  ( A. z e. ran F ph <-> A. z e. { w | E. x e. A E. y e. B w = C } ph )
5 eqeq1 
 |-  ( w = z -> ( w = C <-> z = C ) )
6 5 2rexbidv 
 |-  ( w = z -> ( E. x e. A E. y e. B w = C <-> E. x e. A E. y e. B z = C ) )
7 6 ralab 
 |-  ( A. z e. { w | E. x e. A E. y e. B w = C } ph <-> A. z ( E. x e. A E. y e. B z = C -> ph ) )
8 ralcom4 
 |-  ( A. x e. A A. z ( E. y e. B z = C -> ph ) <-> A. z A. x e. A ( E. y e. B z = C -> ph ) )
9 r19.23v 
 |-  ( A. x e. A ( E. y e. B z = C -> ph ) <-> ( E. x e. A E. y e. B z = C -> ph ) )
10 9 albii 
 |-  ( A. z A. x e. A ( E. y e. B z = C -> ph ) <-> A. z ( E. x e. A E. y e. B z = C -> ph ) )
11 8 10 bitr2i 
 |-  ( A. z ( E. x e. A E. y e. B z = C -> ph ) <-> A. x e. A A. z ( E. y e. B z = C -> ph ) )
12 4 7 11 3bitri 
 |-  ( A. z e. ran F ph <-> A. x e. A A. z ( E. y e. B z = C -> ph ) )
13 ralcom4 
 |-  ( A. y e. B A. z ( z = C -> ph ) <-> A. z A. y e. B ( z = C -> ph ) )
14 r19.23v 
 |-  ( A. y e. B ( z = C -> ph ) <-> ( E. y e. B z = C -> ph ) )
15 14 albii 
 |-  ( A. z A. y e. B ( z = C -> ph ) <-> A. z ( E. y e. B z = C -> ph ) )
16 13 15 bitri 
 |-  ( A. y e. B A. z ( z = C -> ph ) <-> A. z ( E. y e. B z = C -> ph ) )
17 nfv 
 |-  F/ z ps
18 17 2 ceqsalg 
 |-  ( C e. V -> ( A. z ( z = C -> ph ) <-> ps ) )
19 18 ralimi 
 |-  ( A. y e. B C e. V -> A. y e. B ( A. z ( z = C -> ph ) <-> ps ) )
20 ralbi 
 |-  ( A. y e. B ( A. z ( z = C -> ph ) <-> ps ) -> ( A. y e. B A. z ( z = C -> ph ) <-> A. y e. B ps ) )
21 19 20 syl 
 |-  ( A. y e. B C e. V -> ( A. y e. B A. z ( z = C -> ph ) <-> A. y e. B ps ) )
22 16 21 bitr3id 
 |-  ( A. y e. B C e. V -> ( A. z ( E. y e. B z = C -> ph ) <-> A. y e. B ps ) )
23 22 ralimi 
 |-  ( A. x e. A A. y e. B C e. V -> A. x e. A ( A. z ( E. y e. B z = C -> ph ) <-> A. y e. B ps ) )
24 ralbi 
 |-  ( A. x e. A ( A. z ( E. y e. B z = C -> ph ) <-> A. y e. B ps ) -> ( A. x e. A A. z ( E. y e. B z = C -> ph ) <-> A. x e. A A. y e. B ps ) )
25 23 24 syl 
 |-  ( A. x e. A A. y e. B C e. V -> ( A. x e. A A. z ( E. y e. B z = C -> ph ) <-> A. x e. A A. y e. B ps ) )
26 12 25 bitrid 
 |-  ( A. x e. A A. y e. B C e. V -> ( A. z e. ran F ph <-> A. x e. A A. y e. B ps ) )