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