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

Metamath Proof Explorer

Theorem elrnmpt1sf

Description: Elementhood in an image set. Same as elrnmpt1s , but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses elrnmpt1sf.1 
|- F/_ x C
elrnmpt1sf.2 
|- F = ( x e. A |-> B )
elrnmpt1sf.3 
|- ( x = D -> B = C )
Assertion elrnmpt1sf 
|- ( ( D e. A /\ C e. V ) -> C e. ran F )

Proof

Step Hyp Ref Expression
1 elrnmpt1sf.1 
 |-  F/_ x C
2 elrnmpt1sf.2 
 |-  F = ( x e. A |-> B )
3 elrnmpt1sf.3 
 |-  ( x = D -> B = C )
4 eqid 
 |-  C = C
5 1 1 nfeq 
 |-  F/ x C = C
6 3 eqeq2d 
 |-  ( x = D -> ( C = B <-> C = C ) )
7 5 6 rspce 
 |-  ( ( D e. A /\ C = C ) -> E. x e. A C = B )
8 4 7 mpan2 
 |-  ( D e. A -> E. x e. A C = B )
9 1 2 elrnmptf 
 |-  ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )
10 9 biimparc 
 |-  ( ( E. x e. A C = B /\ C e. V ) -> C e. ran F )
11 8 10 sylan 
 |-  ( ( D e. A /\ C e. V ) -> C e. ran F )