Theorem rexrnmpt

Description: A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker rexrnmptw when possible. (Contributed by Mario Carneiro, 20-Aug-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ralrnmpt.1	|- F = ( x e. A |-> B )
	ralrnmpt.2	|- ( y = B -> ( ps <-> ch ) )
Assertion	rexrnmpt	|- ( A. x e. A B e. V -> ( E. y e. ran F ps <-> E. x e. A ch ) )

Proof

Step	Hyp	Ref	Expression
1		ralrnmpt.1	|- F = ( x e. A |-> B )
2		ralrnmpt.2	|- ( y = B -> ( ps <-> ch ) )
3	2	notbid	|- ( y = B -> ( -. ps <-> -. ch ) )
4	1 3	ralrnmpt	|- ( A. x e. A B e. V -> ( A. y e. ran F -. ps <-> A. x e. A -. ch ) )
5	4	notbid	|- ( A. x e. A B e. V -> ( -. A. y e. ran F -. ps <-> -. A. x e. A -. ch ) )
6		dfrex2	|- ( E. y e. ran F ps <-> -. A. y e. ran F -. ps )
7		dfrex2	|- ( E. x e. A ch <-> -. A. x e. A -. ch )
8	5 6 7	3bitr4g	|- ( A. x e. A B e. V -> ( E. y e. ran F ps <-> E. x e. A ch ) )