Theorem rnmpt 5853

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 5852	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5154	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2766	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5835	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3069	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2809	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2776	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  {cab 2715  ∃wrex 3064  {copab 5132   ↦ cmpt 5153  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  elrnmpt  5854  elrnmpt1  5856  elrnmptg  5857  dfiun3g  5862  dfiin3g  5863  fnrnfv  6811  fmpt  6966  fnasrn  6999  fliftf  7166  abrexexg  7777  fo1st  7824  fo2nd  7825  fsplitfpar  7930  qliftf  8552  abrexfi  9049  iinfi  9106  tz9.12lem1  9476  infmap2  9905  cfslb2n  9955  fin23lem29  10028  fin23lem30  10029  fin1a2lem11  10097  ac6num  10166  rankcf  10464  tskuni  10470  negfi  11854  4sqlem11  16584  4sqlem12  16585  vdwapval  16602  vdwlem6  16615  quslem  17171  smndex2dnrinv  18469  conjnmzb  18784  pmtrprfvalrn  19011  sylow1lem2  19119  sylow3lem1  19147  sylow3lem2  19148  ablsimpgfind  19628  ellspd  20919  rnascl  21005  iinopn  21959  restco  22223  pnrmopn  22402  cncmp  22451  discmp  22457  comppfsc  22591  alexsublem  23103  ptcmplem3  23113  snclseqg  23175  prdsxmetlem  23429  prdsbl  23553  xrhmeo  24015  pi1xfrf  24122  pi1cof  24128  iunmbl  24622  voliun  24623  itg1addlem4  24768  itg1addlem4OLD  24769  i1fmulc  24773  mbfi1fseqlem4  24788  itg2monolem1  24820  aannenlem2  25394  2lgslem1b  26445  mptelee  27166  disjrnmpt  30825  ofrn2  30878  abrexct  30953  abrexctf  30955  nsgqusf1olem2  31501  esumc  31919  esumrnmpt  31920  carsgclctunlem3  32187  eulerpartlemt  32238  bdayfo  33807  nosupno  33833  noinfno  33848  fobigcup  34129  ptrest  35703  areacirclem2  35793  istotbnd3  35856  sstotbnd  35860  dfqs2  40138  rnasclg  40149  rmxypairf1o  40649  hbtlem6  40870  elrnmptf  42607  fnrnafv  44541  fundcmpsurinjlem1  44738  imasetpreimafvbijlemfo  44745  fargshiftfo  44782