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 ) )