Theorem rnmpt 5904

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 5901	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5168	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2760	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5884	. 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 5148   ↦ cmpt 5167  ran crn 5623

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 5231  ax-pr 5368

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  elrnmpt  5905  elrnmpt1  5907  elrnmptg  5908  dfiun3g  5915  dfiin3g  5916  fnrnfv  6891  fmpt  7054  fnasrn  7090  fliftf  7261  fo1st  7953  fo2nd  7954  fsplitfpar  8059  dfqs2  8641  qliftf  8743  abrexfi  9253  iinfi  9321  tz9.12lem1  9700  infmap2  10128  cfslb2n  10179  fin23lem29  10252  fin23lem30  10253  fin1a2lem11  10321  ac6num  10390  rankcf  10689  tskuni  10695  negfi  12094  4sqlem11  16915  4sqlem12  16916  vdwapval  16933  vdwlem6  16946  quslem  17496  smndex2dnrinv  18875  conjnmzb  19217  pmtrprfvalrn  19452  sylow1lem2  19563  sylow3lem1  19591  sylow3lem2  19592  ablsimpgfind  20076  pzriprnglem10  21478  ellspd  21790  rnascl  21879  iinopn  22876  restco  23138  pnrmopn  23317  cncmp  23366  discmp  23372  comppfsc  23506  alexsublem  24018  ptcmplem3  24028  snclseqg  24090  prdsxmetlem  24342  prdsbl  24465  xrhmeo  24922  pi1xfrf  25029  pi1cof  25035  iunmbl  25529  voliun  25530  itg1addlem4  25675  i1fmulc  25679  mbfi1fseqlem4  25694  itg2monolem1  25726  aannenlem2  26308  2lgslem1b  27374  bdayfo  27660  nosupno  27686  noinfno  27701  addsuniflem  28012  mpteleeOLD  28983  disjrnmpt  32675  ofrn2  32733  abrexct  32808  abrexctf  32810  qusbas2  33486  nsgqusf1olem2  33494  esumc  34216  esumrnmpt  34217  carsgclctunlem3  34485  eulerpartlemt  34536  fobigcup  36101  ptrest  37951  areacirclem2  38041  istotbnd3  38103  sstotbnd  38107  rnasclg  42955  rmxypairf1o  43354  hbtlem6  43572  onsucrn  43714  elrnmptf  45626  fnrnafv  47607  fundcmpsurinjlem1  47855  imasetpreimafvbijlemfo  47862  fargshiftfo  47899