Theorem rnmpt 5968

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

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  {cab 2714  ∃wrex 3070  {copab 5205   ↦ cmpt 5225  ran crn 5686

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-cnv 5693  df-dm 5695  df-rn 5696

This theorem is referenced by:  elrnmpt  5969  elrnmpt1  5971  elrnmptg  5972  dfiun3g  5978  dfiin3g  5979  fnrnfv  6968  fmpt  7130  fnasrn  7165  fliftf  7335  abrexexgOLD  7986  fo1st  8034  fo2nd  8035  fsplitfpar  8143  qliftf  8845  abrexfi  9392  iinfi  9457  tz9.12lem1  9827  infmap2  10257  cfslb2n  10308  fin23lem29  10381  fin23lem30  10382  fin1a2lem11  10450  ac6num  10519  rankcf  10817  tskuni  10823  negfi  12217  4sqlem11  16993  4sqlem12  16994  vdwapval  17011  vdwlem6  17024  quslem  17588  smndex2dnrinv  18928  conjnmzb  19271  pmtrprfvalrn  19506  sylow1lem2  19617  sylow3lem1  19645  sylow3lem2  19646  ablsimpgfind  20130  pzriprnglem10  21501  ellspd  21822  rnascl  21911  iinopn  22908  restco  23172  pnrmopn  23351  cncmp  23400  discmp  23406  comppfsc  23540  alexsublem  24052  ptcmplem3  24062  snclseqg  24124  prdsxmetlem  24378  prdsbl  24504  xrhmeo  24977  pi1xfrf  25086  pi1cof  25092  iunmbl  25588  voliun  25589  itg1addlem4  25734  i1fmulc  25738  mbfi1fseqlem4  25753  itg2monolem1  25785  aannenlem2  26371  2lgslem1b  27436  bdayfo  27722  nosupno  27748  noinfno  27763  addsuniflem  28034  mptelee  28910  disjrnmpt  32598  ofrn2  32650  abrexct  32728  abrexctf  32730  qusbas2  33434  nsgqusf1olem2  33442  esumc  34052  esumrnmpt  34053  carsgclctunlem3  34322  eulerpartlemt  34373  fobigcup  35901  ptrest  37626  areacirclem2  37716  istotbnd3  37778  sstotbnd  37782  dfqs2  42278  rnasclg  42509  rmxypairf1o  42923  hbtlem6  43141  onsucrn  43284  elrnmptf  45186  fnrnafv  47174  fundcmpsurinjlem1  47385  imasetpreimafvbijlemfo  47392  fargshiftfo  47429