Theorem rnmpt 5933

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 5930	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5182	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2785	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5913	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3087	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2829	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2795	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 399   = wceq 1560  ∃wex 1799   ∈ wcel 2142  {cab 2740  ∃wrex 3086  {copab 5162   ↦ cmpt 5181  ran crn 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-cnv 5655  df-dm 5657  df-rn 5658

This theorem is referenced by:  elrnmpt  5934  elrnmpt1  5936  elrnmptg  5937  dfiun3g  5944  dfiin3g  5945  fnrnfv  6926  fmpt  7091  fnasrn  7127  fliftf  7299  fo1st  7990  fo2nd  7991  fsplitfpar  8097  dfqs2  8685  qliftf  8787  abrexfi  9295  iinfi  9363  tz9.12lem1  9745  infmap2  10173  cfslb2n  10225  fin23lem29  10298  fin23lem30  10299  fin1a2lem11  10367  ac6num  10436  rankcf  10735  tskuni  10741  negfi  12141  4sqlem11  16991  4sqlem12  16992  vdwapval  17009  vdwlem6  17022  quslem  17573  smndex2dnrinv  18952  conjnmzb  19293  pmtrprfvalrn  19528  sylow1lem2  19639  sylow3lem1  19667  sylow3lem2  19668  ablsimpgfind  20152  pzriprnglem10  21539  ellspd  21851  rnascl  21940  iinopn  22959  restco  23221  pnrmopn  23400  cncmp  23449  discmp  23455  comppfsc  23589  alexsublem  24101  ptcmplem3  24111  snclseqg  24173  prdsxmetlem  24425  prdsbl  24548  xrhmeo  25005  pi1xfrf  25112  pi1cof  25118  iunmbl  25612  voliun  25613  itg1addlem4  25758  i1fmulc  25762  mbfi1fseqlem4  25777  itg2monolem1  25809  aannenlem2  26390  2lgslem1b  27453  bdayfo  27738  nosupno  27764  noinfno  27779  addsuniflem  28091  mpteleeOLD  29093  disjrnmpt  32782  ofrn2  32839  abrexct  32914  abrexctf  32916  qusbas2  33589  nsgqusf1olem2  33597  esumc  34345  esumrnmpt  34346  carsgclctunlem3  34614  eulerpartlemt  34665  vonf1oonfo  35455  fobigcup  36245  ptrest  38115  areacirclem2  38205  istotbnd3  38267  sstotbnd  38271  rnasclg  43118  rmxypairf1o  43485  hbtlem6  43703  onsucrn  43845  elrnmptf  45756  fnrnafv  47753  fundcmpsurinjlem1  48001  imasetpreimafvbijlemfo  48008  fargshiftfo  48045