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

Metamath Proof Explorer

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) Avoid ax-13 . (Revised by GG, 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 ) )