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

Theorem rnmpt 5079
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 5078 . 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 4232 . . . 4  |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
42, 3eqtri 2428 . . 3  |-  F  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  =  B ) }
54rneqi 5059 . 2  |-  ran  F  =  ran  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
6 df-rex 2676 . . 3  |-  ( E. x  e.  A  y  =  B  <->  E. x
( x  e.  A  /\  y  =  B
) )
76abbii 2520 . 2  |-  { y  |  E. x  e.  A  y  =  B }  =  { y  |  E. x ( x  e.  A  /\  y  =  B ) }
81, 5, 73eqtr4i 2438 1  |-  ran  F  =  { y  |  E. x  e.  A  y  =  B }
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1721   {cab 2394   E.wrex 2671   {copab 4229    e. cmpt 4230   ran crn 4842
This theorem is referenced by:  elrnmpt  5080  elrnmpt1  5082  elrnmptg  5083  dfiun3g  5085  dfiin3g  5086  fnrnfv  5736  fmpt  5853  fnasrn  5875  abrexex  5946  abrexexg  5947  fliftf  6000  fo1st  6329  fo2nd  6330  qliftf  6955  abrexfi  7369  iinfi  7384  tz9.12lem1  7673  infmap2  8058  cfslb2n  8108  fin23lem29  8181  fin23lem30  8182  fin1a2lem11  8250  ac6num  8319  rankcf  8612  tskuni  8618  gruiun  8634  4sqlem11  13282  4sqlem12  13283  vdwapval  13300  vdwlem6  13313  divslem  13727  conjnmzb  14999  sylow1lem2  15192  sylow3lem1  15220  sylow3lem2  15221  rnascl  16360  iinopn  16934  restco  17186  pnrmopn  17365  cncmp  17413  discmp  17419  alexsublem  18032  ptcmplem3  18042  snclseqg  18102  prdsxmetlem  18355  prdsbl  18478  xrhmeo  18928  pi1xfrf  19035  pi1cof  19041  iunmbl  19404  voliun  19405  itg1addlem4  19548  i1fmulc  19552  mbfi1fseqlem4  19567  itg2monolem1  19599  aannenlem2  20203  nbgraf1olem5  21412  fargshiftfo  21582  efghgrp  21918  circgrp  21919  ofrn2  24010  abrexct  24068  abrexctf  24070  esumc  24403  bdayfo  25547  fobigcup  25658  mptelee  25742  areacirclem4  26187  comppfsc  26281  istotbnd3  26374  sstotbnd  26378  rmxypairf1o  26868  ellspd  27126  hbtlem6  27205  fnrnafv  27897
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177  df-opab 4231  df-mpt 4232  df-cnv 4849  df-dm 4851  df-rn 4852
  Copyright terms: Public domain W3C validator