Theorem rnmpt 5953

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 5952	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5232	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2761	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5935	. 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 5210   ↦ cmpt 5231  ran crn 5677

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 5299  ax-nul 5306  ax-pr 5427

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-cnv 5684  df-dm 5686  df-rn 5687

This theorem is referenced by:  elrnmpt  5954  elrnmpt1  5956  elrnmptg  5957  dfiun3g  5962  dfiin3g  5963  fnrnfv  6949  fmpt  7107  fnasrn  7140  fliftf  7309  abrexexgOLD  7945  fo1st  7992  fo2nd  7993  fsplitfpar  8101  qliftf  8796  abrexfi  9349  iinfi  9409  tz9.12lem1  9779  infmap2  10210  cfslb2n  10260  fin23lem29  10333  fin23lem30  10334  fin1a2lem11  10402  ac6num  10471  rankcf  10769  tskuni  10775  negfi  12160  4sqlem11  16885  4sqlem12  16886  vdwapval  16903  vdwlem6  16916  quslem  17486  smndex2dnrinv  18793  conjnmzb  19122  pmtrprfvalrn  19351  sylow1lem2  19462  sylow3lem1  19490  sylow3lem2  19491  ablsimpgfind  19975  ellspd  21349  rnascl  21437  iinopn  22396  restco  22660  pnrmopn  22839  cncmp  22888  discmp  22894  comppfsc  23028  alexsublem  23540  ptcmplem3  23550  snclseqg  23612  prdsxmetlem  23866  prdsbl  23992  xrhmeo  24454  pi1xfrf  24561  pi1cof  24567  iunmbl  25062  voliun  25063  itg1addlem4  25208  itg1addlem4OLD  25209  i1fmulc  25213  mbfi1fseqlem4  25228  itg2monolem1  25260  aannenlem2  25834  2lgslem1b  26885  bdayfo  27170  nosupno  27196  noinfno  27211  addsuniflem  27474  mptelee  28143  disjrnmpt  31804  ofrn2  31853  abrexct  31929  abrexctf  31931  qusbas2  32506  nsgqusf1olem2  32514  esumc  33038  esumrnmpt  33039  carsgclctunlem3  33308  eulerpartlemt  33359  fobigcup  34861  ptrest  36476  areacirclem2  36566  istotbnd3  36628  sstotbnd  36632  dfqs2  41057  rnasclg  41071  rmxypairf1o  41636  hbtlem6  41857  onsucrn  42007  elrnmptf  43864  fnrnafv  45857  fundcmpsurinjlem1  46053  imasetpreimafvbijlemfo  46060  fargshiftfo  46097