Metamath Proof Explorer

Theorem elrnmpt1

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis rnmpt.1 
|- F = ( x e. A |-> B )
Assertion elrnmpt1 
|- ( ( x e. A /\ B e. V ) -> B e. ran F )

Proof

Step Hyp Ref Expression
1 rnmpt.1 
 |-  F = ( x e. A |-> B )
2 vex 
 |-  x e. _V
3 id 
 |-  ( x = z -> x = z )
4 csbeq1a 
 |-  ( x = z -> A = [_ z / x ]_ A )
5 3 4 eleq12d 
 |-  ( x = z -> ( x e. A <-> z e. [_ z / x ]_ A ) )
6 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
7 6 biantrud 
 |-  ( x = z -> ( z e. [_ z / x ]_ A <-> ( z e. [_ z / x ]_ A /\ B = [_ z / x ]_ B ) ) )
8 5 7 bitr2d 
 |-  ( x = z -> ( ( z e. [_ z / x ]_ A /\ B = [_ z / x ]_ B ) <-> x e. A ) )
9 8 equcoms 
 |-  ( z = x -> ( ( z e. [_ z / x ]_ A /\ B = [_ z / x ]_ B ) <-> x e. A ) )
10 2 9 spcev 
 |-  ( x e. A -> E. z ( z e. [_ z / x ]_ A /\ B = [_ z / x ]_ B ) )
11 df-rex 
 |-  ( E. x e. A y = B <-> E. x ( x e. A /\ y = B ) )
12 nfv 
 |-  F/ z ( x e. A /\ y = B )
13 nfcsb1v 
 |-  F/_ x [_ z / x ]_ A
14 13 nfcri 
 |-  F/ x z e. [_ z / x ]_ A
15 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
16 15 nfeq2 
 |-  F/ x y = [_ z / x ]_ B
17 14 16 nfan 
 |-  F/ x ( z e. [_ z / x ]_ A /\ y = [_ z / x ]_ B )
18 6 eqeq2d 
 |-  ( x = z -> ( y = B <-> y = [_ z / x ]_ B ) )
19 5 18 anbi12d 
 |-  ( x = z -> ( ( x e. A /\ y = B ) <-> ( z e. [_ z / x ]_ A /\ y = [_ z / x ]_ B ) ) )
20 12 17 19 cbvexv1 
 |-  ( E. x ( x e. A /\ y = B ) <-> E. z ( z e. [_ z / x ]_ A /\ y = [_ z / x ]_ B ) )
21 11 20 bitri 
 |-  ( E. x e. A y = B <-> E. z ( z e. [_ z / x ]_ A /\ y = [_ z / x ]_ B ) )
22 eqeq1 
 |-  ( y = B -> ( y = [_ z / x ]_ B <-> B = [_ z / x ]_ B ) )
23 22 anbi2d 
 |-  ( y = B -> ( ( z e. [_ z / x ]_ A /\ y = [_ z / x ]_ B ) <-> ( z e. [_ z / x ]_ A /\ B = [_ z / x ]_ B ) ) )
24 23 exbidv 
 |-  ( y = B -> ( E. z ( z e. [_ z / x ]_ A /\ y = [_ z / x ]_ B ) <-> E. z ( z e. [_ z / x ]_ A /\ B = [_ z / x ]_ B ) ) )
25 21 24 bitrid 
 |-  ( y = B -> ( E. x e. A y = B <-> E. z ( z e. [_ z / x ]_ A /\ B = [_ z / x ]_ B ) ) )
26 1 rnmpt 
 |-  ran F = { y | E. x e. A y = B }
27 25 26 elab2g 
 |-  ( B e. V -> ( B e. ran F <-> E. z ( z e. [_ z / x ]_ A /\ B = [_ z / x ]_ B ) ) )
28 10 27 syl5ibr 
 |-  ( B e. V -> ( x e. A -> B e. ran F ) )
29 28 impcom 
 |-  ( ( x e. A /\ B e. V ) -> B e. ran F )