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

Metamath Proof Explorer

Theorem rexrnmpo

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 rexrnmpo 
|- ( A. x e. A A. y e. B C e. V -> ( E. z e. ran F ph <-> E. x e. A E. 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 2 notbid 
 |-  ( z = C -> ( -. ph <-> -. ps ) )
4 1 3 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 ) )
5 4 notbid 
 |-  ( 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 ) )
6 dfrex2 
 |-  ( E. z e. ran F ph <-> -. A. z e. ran F -. ph )
7 dfrex2 
 |-  ( E. y e. B ps <-> -. A. y e. B -. ps )
8 7 rexbii 
 |-  ( E. x e. A E. y e. B ps <-> E. x e. A -. A. y e. B -. ps )
9 rexnal 
 |-  ( E. x e. A -. A. y e. B -. ps <-> -. A. x e. A A. y e. B -. ps )
10 8 9 bitri 
 |-  ( E. x e. A E. y e. B ps <-> -. A. x e. A A. y e. B -. ps )
11 5 6 10 3bitr4g 
 |-  ( A. x e. A A. y e. B C e. V -> ( E. z e. ran F ph <-> E. x e. A E. y e. B ps ) )