Theorem rnmpt 5237

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

Step	Hyp	Ref	Expression
1		rnopab 5236	. 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 4499	. . . 4 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
4	2, 3	eqtri 2483	. . 3 |- F = { <. x , y >. | ( x e. A /\ y = B ) }
5	4	rneqi 5218	. 2 |- ran F = ran { <. x , y >. | ( x e. A /\ y = B ) }
6		df-rex 2810	. . 3 |- ( E. x e. A y = B <-> E. x ( x e. A /\ y = B ) )
7	6	abbii 2588	. 2 |- { y | E. x e. A y = B } = { y | E. x ( x e. A /\ y = B ) }
8	1, 5, 7	3eqtr4i 2493	1 |- ran F = { y | E. x e. A y = B }

Syntax hints:   /\ wa 367   = wceq 1398   E.wex 1617   e. wcel 1823   {cab 2439   E.wrex 2805   {copab 4496   |-> cmpt 4497   ran crn 4989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-mpt 4499  df-cnv 4996  df-dm 4998  df-rn 4999

This theorem is referenced by:  elrnmpt  5238  elrnmpt1  5240  elrnmptg  5241  dfiun3g  5244  dfiin3g  5245  fnrnfv  5894  fmpt  6028  fnasrn  6053  fliftf  6188  abrexex  6747  abrexexg  6748  fo1st  6793  fo2nd  6794  qliftf  7391  abrexfi  7812  iinfi  7869  tz9.12lem1  8196  infmap2  8589  cfslb2n  8639  fin23lem29  8712  fin23lem30  8713  fin1a2lem11  8781  ac6num  8850  rankcf  9144  tskuni  9150  4sqlem11  14557  4sqlem12  14558  vdwapval  14575  vdwlem6  14588  quslem  15032  conjnmzb  16500  pmtrprfvalrn  16712  sylow1lem2  16818  sylow3lem1  16846  sylow3lem2  16847  rnascl  18187  ellspd  19004  iinopn  19578  restco  19832  pnrmopn  20011  cncmp  20059  discmp  20065  comppfsc  20199  alexsublem  20710  ptcmplem3  20720  snclseqg  20780  prdsxmetlem  21037  prdsbl  21160  xrhmeo  21612  pi1xfrf  21719  pi1cof  21725  iunmbl  22129  voliun  22130  itg1addlem4  22272  i1fmulc  22276  mbfi1fseqlem4  22291  itg2monolem1  22323  aannenlem2  22891  mptelee  24400  nbgraf1olem5  24647  fargshiftfo  24840  efghgrpOLD  25573  circgrpOLD  25574  disjrnmpt  27656  ofrn2  27701  abrexct  27773  abrexctf  27775  esumc  28280  esumrnmpt  28281  carsgclctunlem3  28528  eulerpartlemt  28574  bdayfo  29675  fobigcup  29778  ptrest  30288  areacirclem2  30348  istotbnd3  30507  sstotbnd  30511  rmxypairf1o  31086  hbtlem6  31319  fnrnafv  32486