MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrnmpt1s Structured version   Unicode version

Theorem elrnmpt1s 5098
Description: Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015.)
Hypotheses
Ref Expression
rnmpt.1  |-  F  =  ( x  e.  A  |->  B )
elrnmpt1s.1  |-  ( x  =  D  ->  B  =  C )
Assertion
Ref Expression
elrnmpt1s  |-  ( ( D  e.  A  /\  C  e.  V )  ->  C  e.  ran  F
)
Distinct variable groups:    x, C    x, A    x, D
Allowed substitution hints:    B( x)    F( x)    V( x)

Proof of Theorem elrnmpt1s
StepHypRef Expression
1 eqid 2422 . . 3  |-  C  =  C
2 elrnmpt1s.1 . . . . 5  |-  ( x  =  D  ->  B  =  C )
32eqeq2d 2436 . . . 4  |-  ( x  =  D  ->  ( C  =  B  <->  C  =  C ) )
43rspcev 3182 . . 3  |-  ( ( D  e.  A  /\  C  =  C )  ->  E. x  e.  A  C  =  B )
51, 4mpan2 675 . 2  |-  ( D  e.  A  ->  E. x  e.  A  C  =  B )
6 rnmpt.1 . . . 4  |-  F  =  ( x  e.  A  |->  B )
76elrnmpt 5097 . . 3  |-  ( C  e.  V  ->  ( C  e.  ran  F  <->  E. x  e.  A  C  =  B ) )
87biimparc 489 . 2  |-  ( ( E. x  e.  A  C  =  B  /\  C  e.  V )  ->  C  e.  ran  F
)
95, 8sylan 473 1  |-  ( ( D  e.  A  /\  C  e.  V )  ->  C  e.  ran  F
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1868   E.wrex 2776    |-> cmpt 4479   ran crn 4851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-mpt 4481  df-cnv 4858  df-dm 4860  df-rn 4861
This theorem is referenced by:  wunex2  9164  dfod2  17203  dprd2dlem1  17662  dprd2da  17663  ordtbaslem  20191  subgntr  21108  opnsubg  21109  tgpconcomp  21114  tsmsxplem1  21154  xrge0gsumle  21838  xrge0tsms  21839  minveclem3b  22357  minveclem3  22358  minveclem4  22361  minveclem3bOLD  22369  minveclem3OLD  22370  minveclem4OLD  22373  efsubm  23487  dchrisum0fno1  24336  xrge0tsmsd  28544  esumcvg  28903  esum2d  28910  msubco  30165  sge0xaddlem1  38063
  Copyright terms: Public domain W3C validator