Theorem rnmpt 5097

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 5096	. 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 4482	. . . 4 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
4	2, 3	eqtri 2452	. . 3 |- F = { <. x , y >. | ( x e. A /\ y = B ) }
5	4	rneqi 5078	. 2 |- ran F = ran { <. x , y >. | ( x e. A /\ y = B ) }
6		df-rex 2782	. . 3 |- ( E. x e. A y = B <-> E. x ( x e. A /\ y = B ) )
7	6	abbii 2557	. 2 |- { y | E. x e. A y = B } = { y | E. x ( x e. A /\ y = B ) }
8	1, 5, 7	3eqtr4i 2462	1 |- ran F = { y | E. x e. A y = B }

Syntax hints:   /\ wa 371   = wceq 1438   E.wex 1660   e. wcel 1869   {cab 2408   E.wrex 2777   {copab 4479   |-> cmpt 4480   ran crn 4852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-mpt 4482  df-cnv 4859  df-dm 4861  df-rn 4862

This theorem is referenced by:  elrnmpt  5098  elrnmpt1  5100  elrnmptg  5101  dfiun3g  5104  dfiin3g  5105  fnrnfv  5925  fmpt  6056  fnasrn  6083  fliftf  6221  abrexex  6779  abrexexg  6780  fo1st  6825  fo2nd  6826  qliftf  7457  abrexfi  7878  iinfi  7935  tz9.12lem1  8261  infmap2  8650  cfslb2n  8700  fin23lem29  8773  fin23lem30  8774  fin1a2lem11  8842  ac6num  8911  rankcf  9204  tskuni  9210  negfi  10556  4sqlem11  14892  4sqlem12  14893  vdwapval  14916  vdwlem6  14929  quslem  15442  conjnmzb  16910  pmtrprfvalrn  17122  sylow1lem2  17244  sylow3lem1  17272  sylow3lem2  17273  rnascl  18560  ellspd  19352  iinopn  19924  restco  20172  pnrmopn  20351  cncmp  20399  discmp  20405  comppfsc  20539  alexsublem  21051  ptcmplem3  21061  snclseqg  21122  prdsxmetlem  21375  prdsbl  21498  xrhmeo  21966  pi1xfrf  22076  pi1cof  22082  iunmbl  22498  voliun  22499  itg1addlem4  22649  i1fmulc  22653  mbfi1fseqlem4  22668  itg2monolem1  22700  aannenlem2  23277  mptelee  24917  nbgraf1olem5  25165  fargshiftfo  25358  efghgrpOLD  26093  circgrpOLD  26094  disjrnmpt  28191  ofrn2  28237  abrexct  28304  abrexctf  28306  esumc  28874  esumrnmpt  28875  carsgclctunlem3  29154  eulerpartlemt  29206  bdayfo  30563  fobigcup  30666  ptrest  31897  areacirclem2  31991  istotbnd3  32061  sstotbnd  32065  rmxypairf1o  35723  hbtlem6  35952  elrnmptf  37348  fnrnafv  38420