Theorem rnmpt 5186

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 5185	. 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 4453	. . . 4 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
4	2, 3	eqtri 2480	. . 3 |- F = { <. x , y >. | ( x e. A /\ y = B ) }
5	4	rneqi 5167	. 2 |- ran F = ran { <. x , y >. | ( x e. A /\ y = B ) }
6		df-rex 2801	. . 3 |- ( E. x e. A y = B <-> E. x ( x e. A /\ y = B ) )
7	6	abbii 2585	. 2 |- { y | E. x e. A y = B } = { y | E. x ( x e. A /\ y = B ) }
8	1, 5, 7	3eqtr4i 2490	1 |- ran F = { y | E. x e. A y = B }

Syntax hints:   /\ wa 369   = wceq 1370   E.wex 1587   e. wcel 1758   {cab 2436   E.wrex 2796   {copab 4450   |-> cmpt 4451   ran crn 4942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-rex 2801  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-br 4394  df-opab 4452  df-mpt 4453  df-cnv 4949  df-dm 4951  df-rn 4952

This theorem is referenced by:  elrnmpt  5187  elrnmpt1  5189  elrnmptg  5190  dfiun3g  5193  dfiin3g  5194  fnrnfv  5840  fmpt  5966  fnasrn  5990  fliftf  6110  abrexex  6654  abrexexg  6655  fo1st  6699  fo2nd  6700  qliftf  7291  abrexfi  7715  iinfi  7771  tz9.12lem1  8098  infmap2  8491  cfslb2n  8541  fin23lem29  8614  fin23lem30  8615  fin1a2lem11  8683  ac6num  8752  rankcf  9048  tskuni  9054  gruiun  9070  4sqlem11  14127  4sqlem12  14128  vdwapval  14145  vdwlem6  14158  divslem  14592  conjnmzb  15892  pmtrprfvalrn  16105  sylow1lem2  16211  sylow3lem1  16239  sylow3lem2  16240  rnascl  17528  ellspd  18348  ellspdOLD  18349  iinopn  18640  restco  18893  pnrmopn  19072  cncmp  19120  discmp  19126  alexsublem  19741  ptcmplem3  19751  snclseqg  19811  prdsxmetlem  20068  prdsbl  20191  xrhmeo  20643  pi1xfrf  20750  pi1cof  20756  iunmbl  21160  voliun  21161  itg1addlem4  21303  i1fmulc  21307  mbfi1fseqlem4  21322  itg2monolem1  21354  aannenlem2  21921  mptelee  23286  nbgraf1olem5  23499  fargshiftfo  23669  efghgrp  24005  circgrp  24006  ofrn2  26102  abrexct  26164  abrexctf  26166  esumc  26643  eulerpartlemt  26891  bdayfo  27953  fobigcup  28068  ptrest  28566  areacirclem2  28626  comppfsc  28720  istotbnd3  28811  sstotbnd  28815  rmxypairf1o  29393  hbtlem6  29626  fnrnafv  30209