Theorem rnmpt 5955

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 5954	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5233	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2761	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5937	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3072	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2803	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2771	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107  {cab 2710  ∃wrex 3071  {copab 5211   ↦ cmpt 5232  ran crn 5678

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 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-mpt 5233  df-cnv 5685  df-dm 5687  df-rn 5688

This theorem is referenced by:  elrnmpt  5956  elrnmpt1  5958  elrnmptg  5959  dfiun3g  5964  dfiin3g  5965  fnrnfv  6952  fmpt  7110  fnasrn  7143  fliftf  7312  abrexexgOLD  7948  fo1st  7995  fo2nd  7996  fsplitfpar  8104  qliftf  8799  abrexfi  9352  iinfi  9412  tz9.12lem1  9782  infmap2  10213  cfslb2n  10263  fin23lem29  10336  fin23lem30  10337  fin1a2lem11  10405  ac6num  10474  rankcf  10772  tskuni  10778  negfi  12163  4sqlem11  16888  4sqlem12  16889  vdwapval  16906  vdwlem6  16919  quslem  17489  smndex2dnrinv  18796  conjnmzb  19127  pmtrprfvalrn  19356  sylow1lem2  19467  sylow3lem1  19495  sylow3lem2  19496  ablsimpgfind  19980  ellspd  21357  rnascl  21445  iinopn  22404  restco  22668  pnrmopn  22847  cncmp  22896  discmp  22902  comppfsc  23036  alexsublem  23548  ptcmplem3  23558  snclseqg  23620  prdsxmetlem  23874  prdsbl  24000  xrhmeo  24462  pi1xfrf  24569  pi1cof  24575  iunmbl  25070  voliun  25071  itg1addlem4  25216  itg1addlem4OLD  25217  i1fmulc  25221  mbfi1fseqlem4  25236  itg2monolem1  25268  aannenlem2  25842  2lgslem1b  26895  bdayfo  27180  nosupno  27206  noinfno  27221  addsuniflem  27484  mptelee  28153  disjrnmpt  31816  ofrn2  31865  abrexct  31941  abrexctf  31943  qusbas2  32517  nsgqusf1olem2  32525  esumc  33049  esumrnmpt  33050  carsgclctunlem3  33319  eulerpartlemt  33370  fobigcup  34872  ptrest  36487  areacirclem2  36577  istotbnd3  36639  sstotbnd  36643  dfqs2  41059  rnasclg  41073  rmxypairf1o  41650  hbtlem6  41871  onsucrn  42021  elrnmptf  43878  fnrnafv  45870  fundcmpsurinjlem1  46066  imasetpreimafvbijlemfo  46073  fargshiftfo  46110  pzriprnglem10  46814