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

Theorem rnmpt 5004
Description: The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypothesis
Ref Expression
rnmpt.1  |-  F  =  ( x  e.  A  |->  B )
Assertion
Ref Expression
rnmpt  |-  ran  F  =  { y  |  E. x  e.  A  y  =  B }
Distinct variable groups:    y, A    y, B    x, y
Allowed substitution hints:    A( x)    B( x)    F( x, y)

Proof of Theorem rnmpt
StepHypRef Expression
1 rnopab 5003 . 2  |-  ran  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }  =  { y  |  E. x ( x  e.  A  /\  y  =  B ) }
2 rnmpt.1 . . . 4  |-  F  =  ( x  e.  A  |->  B )
3 df-mpt 4158 . . . 4  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
42, 3eqtri 2378 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
54rneqi 4984 . 2  |-  ran  F  =  ran  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
6 df-rex 2625 . . 3  |-  ( E. x  e.  A  y  =  B  <->  E. x
( x  e.  A  /\  y  =  B
) )
76abbii 2470 . 2  |-  { y  |  E. x  e.  A  y  =  B }  =  { y  |  E. x ( x  e.  A  /\  y  =  B ) }
81, 5, 73eqtr4i 2388 1  |-  ran  F  =  { y  |  E. x  e.  A  y  =  B }
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1541    = wceq 1642    e. wcel 1710   {cab 2344   E.wrex 2620   {copab 4155    e. cmpt 4156   ran crn 4769
This theorem is referenced by:  elrnmpt  5005  elrnmpt1  5007  elrnmptg  5008  dfiun3g  5010  dfiin3g  5011  fnrnfv  5649  fmpt  5761  fnasrn  5782  abrexex  5846  abrexexg  5847  fliftf  5898  fo1st  6223  fo2nd  6224  qliftf  6831  abrexfi  7243  iinfi  7258  tz9.12lem1  7546  infmap2  7931  cfslb2n  7981  fin23lem29  8054  fin23lem30  8055  fin1a2lem11  8123  ac6num  8193  rankcf  8486  tskuni  8492  gruiun  8508  4sqlem11  13093  4sqlem12  13094  vdwapval  13111  vdwlem6  13124  divslem  13538  conjnmzb  14810  sylow1lem2  15003  sylow3lem1  15031  sylow3lem2  15032  rnascl  16175  iinopn  16748  restco  16995  pnrmopn  17171  cncmp  17219  discmp  17225  alexsublem  17834  ptcmplem3  17844  snclseqg  17894  prdsxmetlem  18028  prdsbl  18133  xrhmeo  18542  pi1xfrf  18649  pi1cof  18655  iunmbl  19008  voliun  19009  itg1addlem4  19152  i1fmulc  19156  mbfi1fseqlem4  19171  itg2monolem1  19203  aannenlem2  19807  efghgrp  21146  circgrp  21147  ofrn2  23254  abrexct  23312  abrexctf  23314  esumc  23712  bdayfo  24887  fobigcup  24998  mptelee  25082  areacirclem4  25519  comppfsc  25631  istotbnd3  25818  sstotbnd  25822  rmxypairf1o  26319  ellspd  26577  hbtlem6  26656  fnrnafv  27350  nbgraf1olem5  27601  fargshiftfo  27744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pr 4293
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4103  df-opab 4157  df-mpt 4158  df-cnv 4776  df-dm 4778  df-rn 4779
  Copyright terms: Public domain W3C validator