Theorem rnmpt 5910

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 5907	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5184	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2752	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5890	. 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 5164   ↦ cmpt 5183  ran crn 5632

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-mpt 5184  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  elrnmpt  5911  elrnmpt1  5913  elrnmptg  5914  dfiun3g  5920  dfiin3g  5921  fnrnfv  6902  fmpt  7064  fnasrn  7099  fliftf  7272  fo1st  7967  fo2nd  7968  fsplitfpar  8074  qliftf  8755  abrexfi  9279  iinfi  9344  tz9.12lem1  9716  infmap2  10146  cfslb2n  10197  fin23lem29  10270  fin23lem30  10271  fin1a2lem11  10339  ac6num  10408  rankcf  10706  tskuni  10712  negfi  12108  4sqlem11  16902  4sqlem12  16903  vdwapval  16920  vdwlem6  16933  quslem  17482  smndex2dnrinv  18818  conjnmzb  19161  pmtrprfvalrn  19394  sylow1lem2  19505  sylow3lem1  19533  sylow3lem2  19534  ablsimpgfind  20018  pzriprnglem10  21376  ellspd  21687  rnascl  21776  iinopn  22765  restco  23027  pnrmopn  23206  cncmp  23255  discmp  23261  comppfsc  23395  alexsublem  23907  ptcmplem3  23917  snclseqg  23979  prdsxmetlem  24232  prdsbl  24355  xrhmeo  24820  pi1xfrf  24929  pi1cof  24935  iunmbl  25430  voliun  25431  itg1addlem4  25576  i1fmulc  25580  mbfi1fseqlem4  25595  itg2monolem1  25627  aannenlem2  26213  2lgslem1b  27279  bdayfo  27565  nosupno  27591  noinfno  27606  addsuniflem  27884  mptelee  28798  disjrnmpt  32487  ofrn2  32537  abrexct  32613  abrexctf  32615  qusbas2  33350  nsgqusf1olem2  33358  esumc  34014  esumrnmpt  34015  carsgclctunlem3  34284  eulerpartlemt  34335  fobigcup  35861  ptrest  37586  areacirclem2  37676  istotbnd3  37738  sstotbnd  37742  dfqs2  42198  rnasclg  42460  rmxypairf1o  42873  hbtlem6  43091  onsucrn  43233  elrnmptf  45148  fnrnafv  47136  fundcmpsurinjlem1  47372  imasetpreimafvbijlemfo  47379  fargshiftfo  47416