Theorem rnmpt 5239

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 5238	. 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 4500	. . . 4 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
4	2, 3	eqtri 2489	. . 3 |- F = { <. x , y >. | ( x e. A /\ y = B ) }
5	4	rneqi 5220	. 2 |- ran F = ran { <. x , y >. | ( x e. A /\ y = B ) }
6		df-rex 2813	. . 3 |- ( E. x e. A y = B <-> E. x ( x e. A /\ y = B ) )
7	6	abbii 2594	. 2 |- { y | E. x e. A y = B } = { y | E. x ( x e. A /\ y = B ) }
8	1, 5, 7	3eqtr4i 2499	1 |- ran F = { y | E. x e. A y = B }

Syntax hints:   /\ wa 369   = wceq 1374   E.wex 1591   e. wcel 1762   {cab 2445   E.wrex 2808   {copab 4497   |-> cmpt 4498   ran crn 4993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-mpt 4500  df-cnv 5000  df-dm 5002  df-rn 5003

This theorem is referenced by:  elrnmpt  5240  elrnmpt1  5242  elrnmptg  5243  dfiun3g  5246  dfiin3g  5247  fnrnfv  5905  fmpt  6033  fnasrn  6058  fliftf  6192  abrexex  6748  abrexexg  6749  fo1st  6794  fo2nd  6795  qliftf  7389  abrexfi  7809  iinfi  7866  tz9.12lem1  8194  infmap2  8587  cfslb2n  8637  fin23lem29  8710  fin23lem30  8711  fin1a2lem11  8779  ac6num  8848  rankcf  9144  tskuni  9150  gruiun  9166  4sqlem11  14321  4sqlem12  14322  vdwapval  14339  vdwlem6  14352  divslem  14787  conjnmzb  16089  pmtrprfvalrn  16302  sylow1lem2  16408  sylow3lem1  16436  sylow3lem2  16437  rnascl  17756  ellspd  18596  ellspdOLD  18597  iinopn  19171  restco  19424  pnrmopn  19603  cncmp  19651  discmp  19657  alexsublem  20272  ptcmplem3  20282  snclseqg  20342  prdsxmetlem  20599  prdsbl  20722  xrhmeo  21174  pi1xfrf  21281  pi1cof  21287  iunmbl  21691  voliun  21692  itg1addlem4  21834  i1fmulc  21838  mbfi1fseqlem4  21853  itg2monolem1  21885  aannenlem2  22452  mptelee  23867  nbgraf1olem5  24107  fargshiftfo  24300  efghgrp  25037  circgrp  25038  ofrn2  27139  abrexct  27201  abrexctf  27203  esumc  27688  eulerpartlemt  27936  bdayfo  28998  fobigcup  29113  ptrest  29612  areacirclem2  29672  comppfsc  29766  istotbnd3  29857  sstotbnd  29861  rmxypairf1o  30438  hbtlem6  30671  fnrnafv  31669