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

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707  ∃wrex 3053  {copab 5154   ↦ cmpt 5173  ran crn 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  elrnmpt  5900  elrnmpt1  5902  elrnmptg  5903  dfiun3g  5909  dfiin3g  5910  fnrnfv  6882  fmpt  7044  fnasrn  7079  fliftf  7252  fo1st  7944  fo2nd  7945  fsplitfpar  8051  qliftf  8732  abrexfi  9242  iinfi  9307  tz9.12lem1  9683  infmap2  10111  cfslb2n  10162  fin23lem29  10235  fin23lem30  10236  fin1a2lem11  10304  ac6num  10373  rankcf  10671  tskuni  10677  negfi  12074  4sqlem11  16867  4sqlem12  16868  vdwapval  16885  vdwlem6  16898  quslem  17447  smndex2dnrinv  18789  conjnmzb  19132  pmtrprfvalrn  19367  sylow1lem2  19478  sylow3lem1  19506  sylow3lem2  19507  ablsimpgfind  19991  pzriprnglem10  21397  ellspd  21709  rnascl  21798  iinopn  22787  restco  23049  pnrmopn  23228  cncmp  23277  discmp  23283  comppfsc  23417  alexsublem  23929  ptcmplem3  23939  snclseqg  24001  prdsxmetlem  24254  prdsbl  24377  xrhmeo  24842  pi1xfrf  24951  pi1cof  24957  iunmbl  25452  voliun  25453  itg1addlem4  25598  i1fmulc  25602  mbfi1fseqlem4  25617  itg2monolem1  25649  aannenlem2  26235  2lgslem1b  27301  bdayfo  27587  nosupno  27613  noinfno  27628  addsuniflem  27913  mptelee  28840  disjrnmpt  32529  ofrn2  32583  abrexct  32659  abrexctf  32661  qusbas2  33343  nsgqusf1olem2  33351  esumc  34018  esumrnmpt  34019  carsgclctunlem3  34288  eulerpartlemt  34339  fobigcup  35874  ptrest  37599  areacirclem2  37689  istotbnd3  37751  sstotbnd  37755  dfqs2  42210  rnasclg  42472  rmxypairf1o  42884  hbtlem6  43102  onsucrn  43244  elrnmptf  45159  fnrnafv  47146  fundcmpsurinjlem1  47382  imasetpreimafvbijlemfo  47389  fargshiftfo  47426