Theorem rnmpt 5522

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 5521	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 4878	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2778	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5503	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3052	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2873	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2788	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 383   = wceq 1628  ∃wex 1849   ∈ wcel 2135  {cab 2742  ∃wrex 3047  {copab 4860   ↦ cmpt 4877  ran crn 5263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pr 5051

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-rex 3052  df-rab 3055  df-v 3338  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-br 4801  df-opab 4861  df-mpt 4878  df-cnv 5270  df-dm 5272  df-rn 5273

This theorem is referenced by:  elrnmpt  5523  elrnmpt1  5525  elrnmptg  5526  dfiun3g  5529  dfiin3g  5530  fnrnfv  6400  fmpt  6540  fnasrn  6570  fliftf  6724  abrexexg  7301  abrexexOLD  7303  fo1st  7349  fo2nd  7350  qliftf  7998  abrexfi  8427  iinfi  8484  tz9.12lem1  8819  infmap2  9228  cfslb2n  9278  fin23lem29  9351  fin23lem30  9352  fin1a2lem11  9420  ac6num  9489  rankcf  9787  tskuni  9793  negfi  11159  4sqlem11  15857  4sqlem12  15858  vdwapval  15875  vdwlem6  15888  quslem  16401  conjnmzb  17892  pmtrprfvalrn  18104  sylow1lem2  18210  sylow3lem1  18238  sylow3lem2  18239  rnascl  19541  ellspd  20339  iinopn  20905  restco  21166  pnrmopn  21345  cncmp  21393  discmp  21399  comppfsc  21533  alexsublem  22045  ptcmplem3  22055  snclseqg  22116  prdsxmetlem  22370  prdsbl  22493  xrhmeo  22942  pi1xfrf  23049  pi1cof  23055  iunmbl  23517  voliun  23518  itg1addlem4  23661  i1fmulc  23665  mbfi1fseqlem4  23680  itg2monolem1  23712  aannenlem2  24279  2lgslem1b  25312  mptelee  25970  disjrnmpt  29701  ofrn2  29747  abrexct  29799  abrexctf  29801  esumc  30418  esumrnmpt  30419  carsgclctunlem3  30687  eulerpartlemt  30738  bdayfo  32130  nosupno  32151  fobigcup  32309  ptrest  33717  areacirclem2  33810  istotbnd3  33879  sstotbnd  33883  rmxypairf1o  37974  hbtlem6  38197  elrnmptf  39862  fnrnafv  41744  fargshiftfo  41884