Theorem rnmpt 5906

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 5903	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5180	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2759	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5886	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3061	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2803	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2769	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  {cab 2714  ∃wrex 3060  {copab 5160   ↦ cmpt 5179  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  elrnmpt  5907  elrnmpt1  5909  elrnmptg  5910  dfiun3g  5917  dfiin3g  5918  fnrnfv  6893  fmpt  7055  fnasrn  7090  fliftf  7261  fo1st  7953  fo2nd  7954  fsplitfpar  8060  qliftf  8742  abrexfi  9252  iinfi  9320  tz9.12lem1  9699  infmap2  10127  cfslb2n  10178  fin23lem29  10251  fin23lem30  10252  fin1a2lem11  10320  ac6num  10389  rankcf  10688  tskuni  10694  negfi  12091  4sqlem11  16883  4sqlem12  16884  vdwapval  16901  vdwlem6  16914  quslem  17464  smndex2dnrinv  18840  conjnmzb  19182  pmtrprfvalrn  19417  sylow1lem2  19528  sylow3lem1  19556  sylow3lem2  19557  ablsimpgfind  20041  pzriprnglem10  21445  ellspd  21757  rnascl  21847  iinopn  22846  restco  23108  pnrmopn  23287  cncmp  23336  discmp  23342  comppfsc  23476  alexsublem  23988  ptcmplem3  23998  snclseqg  24060  prdsxmetlem  24312  prdsbl  24435  xrhmeo  24900  pi1xfrf  25009  pi1cof  25015  iunmbl  25510  voliun  25511  itg1addlem4  25656  i1fmulc  25660  mbfi1fseqlem4  25675  itg2monolem1  25707  aannenlem2  26293  2lgslem1b  27359  bdayfo  27645  nosupno  27671  noinfno  27686  addsuniflem  27997  mpteleeOLD  28968  disjrnmpt  32660  ofrn2  32718  abrexct  32794  abrexctf  32796  qusbas2  33487  nsgqusf1olem2  33495  esumc  34208  esumrnmpt  34209  carsgclctunlem3  34477  eulerpartlemt  34528  fobigcup  36092  ptrest  37820  areacirclem2  37910  istotbnd3  37972  sstotbnd  37976  dfqs2  42493  rnasclg  42754  rmxypairf1o  43153  hbtlem6  43371  onsucrn  43513  elrnmptf  45425  fnrnafv  47408  fundcmpsurinjlem1  47644  imasetpreimafvbijlemfo  47651  fargshiftfo  47688