Theorem rnmpt 5914

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	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
rnmpt	⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥,𝑦)

Proof of Theorem rnmpt

Step	Hyp	Ref	Expression
1		rnopab 5911	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5182	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2760	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5894	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3063	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2804	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2770	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715  ∃wrex 3062  {copab 5162   ↦ cmpt 5181  ran crn 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  elrnmpt  5915  elrnmpt1  5917  elrnmptg  5918  dfiun3g  5925  dfiin3g  5926  fnrnfv  6901  fmpt  7064  fnasrn  7100  fliftf  7271  fo1st  7963  fo2nd  7964  fsplitfpar  8070  dfqs2  8652  qliftf  8754  abrexfi  9264  iinfi  9332  tz9.12lem1  9711  infmap2  10139  cfslb2n  10190  fin23lem29  10263  fin23lem30  10264  fin1a2lem11  10332  ac6num  10401  rankcf  10700  tskuni  10706  negfi  12103  4sqlem11  16895  4sqlem12  16896  vdwapval  16913  vdwlem6  16926  quslem  17476  smndex2dnrinv  18852  conjnmzb  19194  pmtrprfvalrn  19429  sylow1lem2  19540  sylow3lem1  19568  sylow3lem2  19569  ablsimpgfind  20053  pzriprnglem10  21457  ellspd  21769  rnascl  21859  iinopn  22858  restco  23120  pnrmopn  23299  cncmp  23348  discmp  23354  comppfsc  23488  alexsublem  24000  ptcmplem3  24010  snclseqg  24072  prdsxmetlem  24324  prdsbl  24447  xrhmeo  24912  pi1xfrf  25021  pi1cof  25027  iunmbl  25522  voliun  25523  itg1addlem4  25668  i1fmulc  25672  mbfi1fseqlem4  25687  itg2monolem1  25719  aannenlem2  26305  2lgslem1b  27371  bdayfo  27657  nosupno  27683  noinfno  27698  addsuniflem  28009  mpteleeOLD  28980  disjrnmpt  32672  ofrn2  32730  abrexct  32805  abrexctf  32807  qusbas2  33499  nsgqusf1olem2  33507  esumc  34229  esumrnmpt  34230  carsgclctunlem3  34498  eulerpartlemt  34549  fobigcup  36114  ptrest  37870  areacirclem2  37960  istotbnd3  38022  sstotbnd  38026  rnasclg  42869  rmxypairf1o  43268  hbtlem6  43486  onsucrn  43628  elrnmptf  45540  fnrnafv  47522  fundcmpsurinjlem1  47758  imasetpreimafvbijlemfo  47765  fargshiftfo  47802