Theorem rnmpt 5098

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 5097	. 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 4476	. . . 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 5079	. 2 |- ran F = ran { <. x , y >. | ( x e. A /\ y = B ) }
6		df-rex 2754	. . 3 |- ( E. x e. A y = B <-> E. x ( x e. A /\ y = B ) )
7	6	abbii 2577	. 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 375   = wceq 1454   E.wex 1673   e. wcel 1897   {cab 2447   E.wrex 2749   {copab 4473   |-> cmpt 4474   ran crn 4853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-mpt 4476  df-cnv 4860  df-dm 4862  df-rn 4863

This theorem is referenced by:  elrnmpt  5099  elrnmpt1  5101  elrnmptg  5102  dfiun3g  5105  dfiin3g  5106  fnrnfv  5933  fmpt  6065  fnasrn  6093  fliftf  6232  abrexex  6793  abrexexg  6794  fo1st  6839  fo2nd  6840  qliftf  7476  abrexfi  7899  iinfi  7956  tz9.12lem1  8283  infmap2  8673  cfslb2n  8723  fin23lem29  8796  fin23lem30  8797  fin1a2lem11  8865  ac6num  8934  rankcf  9227  tskuni  9233  negfi  10581  4sqlem11  14947  4sqlem12  14948  vdwapval  14971  vdwlem6  14984  quslem  15497  conjnmzb  16965  pmtrprfvalrn  17177  sylow1lem2  17299  sylow3lem1  17327  sylow3lem2  17328  rnascl  18615  ellspd  19408  iinopn  19980  restco  20228  pnrmopn  20407  cncmp  20455  discmp  20461  comppfsc  20595  alexsublem  21107  ptcmplem3  21117  snclseqg  21178  prdsxmetlem  21431  prdsbl  21554  xrhmeo  22022  pi1xfrf  22132  pi1cof  22138  iunmbl  22554  voliun  22555  itg1addlem4  22705  i1fmulc  22709  mbfi1fseqlem4  22724  itg2monolem1  22756  aannenlem2  23333  mptelee  24973  nbgraf1olem5  25221  fargshiftfo  25414  efghgrpOLD  26149  circgrpOLD  26150  disjrnmpt  28243  ofrn2  28289  abrexct  28352  abrexctf  28354  esumc  28920  esumrnmpt  28921  carsgclctunlem3  29200  eulerpartlemt  29252  bdayfo  30612  fobigcup  30715  ptrest  31983  areacirclem2  32077  istotbnd3  32147  sstotbnd  32151  rmxypairf1o  35803  hbtlem6  36032  elrnmptf  37491  fnrnafv  38701