Theorem rnmpt 5867

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 5866	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5159	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2767	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5849	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3071	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2809	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2777	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2107  {cab 2716  ∃wrex 3066  {copab 5137   ↦ cmpt 5158  ran crn 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-mpt 5159  df-cnv 5598  df-dm 5600  df-rn 5601

This theorem is referenced by:  elrnmpt  5868  elrnmpt1  5870  elrnmptg  5871  dfiun3g  5876  dfiin3g  5877  fnrnfv  6838  fmpt  6993  fnasrn  7026  fliftf  7195  abrexexgOLD  7813  fo1st  7860  fo2nd  7861  fsplitfpar  7968  qliftf  8603  abrexfi  9128  iinfi  9185  tz9.12lem1  9554  infmap2  9983  cfslb2n  10033  fin23lem29  10106  fin23lem30  10107  fin1a2lem11  10175  ac6num  10244  rankcf  10542  tskuni  10548  negfi  11933  4sqlem11  16665  4sqlem12  16666  vdwapval  16683  vdwlem6  16696  quslem  17263  smndex2dnrinv  18563  conjnmzb  18878  pmtrprfvalrn  19105  sylow1lem2  19213  sylow3lem1  19241  sylow3lem2  19242  ablsimpgfind  19722  ellspd  21018  rnascl  21104  iinopn  22060  restco  22324  pnrmopn  22503  cncmp  22552  discmp  22558  comppfsc  22692  alexsublem  23204  ptcmplem3  23214  snclseqg  23276  prdsxmetlem  23530  prdsbl  23656  xrhmeo  24118  pi1xfrf  24225  pi1cof  24231  iunmbl  24726  voliun  24727  itg1addlem4  24872  itg1addlem4OLD  24873  i1fmulc  24877  mbfi1fseqlem4  24892  itg2monolem1  24924  aannenlem2  25498  2lgslem1b  26549  mptelee  27272  disjrnmpt  30933  ofrn2  30986  abrexct  31060  abrexctf  31062  nsgqusf1olem2  31608  esumc  32028  esumrnmpt  32029  carsgclctunlem3  32296  eulerpartlemt  32347  bdayfo  33889  nosupno  33915  noinfno  33930  fobigcup  34211  ptrest  35785  areacirclem2  35875  istotbnd3  35938  sstotbnd  35942  dfqs2  40219  rnasclg  40230  rmxypairf1o  40740  hbtlem6  40961  elrnmptf  42725  fnrnafv  44665  fundcmpsurinjlem1  44861  imasetpreimafvbijlemfo  44868  fargshiftfo  44905