Theorem rnmpt 5899

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 5896	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5154	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2762	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5879	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3064	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2806	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2772	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  {cab 2717  ∃wrex 3063  {copab 5134   ↦ cmpt 5153  ran crn 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-mpt 5154  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  elrnmpt  5900  elrnmpt1  5902  elrnmptg  5903  dfiun3g  5910  dfiin3g  5911  fnrnfv  6886  fmpt  7051  fnasrn  7087  fliftf  7259  fo1st  7951  fo2nd  7952  fsplitfpar  8057  dfqs2  8640  qliftf  8742  abrexfi  9252  iinfi  9320  tz9.12lem1  9702  infmap2  10130  cfslb2n  10181  fin23lem29  10254  fin23lem30  10255  fin1a2lem11  10323  ac6num  10392  rankcf  10691  tskuni  10697  negfi  12096  4sqlem11  16917  4sqlem12  16918  vdwapval  16935  vdwlem6  16948  quslem  17498  smndex2dnrinv  18877  conjnmzb  19219  pmtrprfvalrn  19454  sylow1lem2  19565  sylow3lem1  19593  sylow3lem2  19594  ablsimpgfind  20078  pzriprnglem10  21465  ellspd  21777  rnascl  21866  iinopn  22885  restco  23147  pnrmopn  23326  cncmp  23375  discmp  23381  comppfsc  23515  alexsublem  24027  ptcmplem3  24037  snclseqg  24099  prdsxmetlem  24351  prdsbl  24474  xrhmeo  24931  pi1xfrf  25038  pi1cof  25044  iunmbl  25538  voliun  25539  itg1addlem4  25684  i1fmulc  25688  mbfi1fseqlem4  25703  itg2monolem1  25735  aannenlem2  26313  2lgslem1b  27373  bdayfo  27659  nosupno  27685  noinfno  27700  addsuniflem  28011  mpteleeOLD  28982  disjrnmpt  32674  ofrn2  32732  abrexct  32807  abrexctf  32809  qusbas2  33489  nsgqusf1olem2  33497  esumc  34235  esumrnmpt  34236  carsgclctunlem3  34504  eulerpartlemt  34555  fobigcup  36126  ptrest  37986  areacirclem2  38076  istotbnd3  38138  sstotbnd  38142  rnasclg  42989  rmxypairf1o  43356  hbtlem6  43574  onsucrn  43716  elrnmptf  45628  fnrnafv  47625  fundcmpsurinjlem1  47873  imasetpreimafvbijlemfo  47880  fargshiftfo  47917