Theorem rexrnmptw

Description: A restricted quantifier over an image set. Version of rexrnmpt with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 20-Aug-2015) (Revised by Gino Giotto, 26-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		rexrnmptw.1	|- F = ( x e. A |-> B )
2		rexrnmptw.2	|- ( y = B -> ( ps <-> ch ) )
3	2	notbid	|- ( y = B -> ( -. ps <-> -. ch ) )
4	1 3	ralrnmptw	|- ( 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 ) )