Theorem rnmpt 5292

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 5291	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 4645	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2632	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5273	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 2902	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2726	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2642	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  ∃wrex 2897  {copab 4642   ↦ cmpt 4643  ran crn 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-mpt 4645  df-cnv 5046  df-dm 5048  df-rn 5049

This theorem is referenced by:  elrnmpt  5293  elrnmpt1  5295  elrnmptg  5296  dfiun3g  5299  dfiin3g  5300  fnrnfv  6152  fmpt  6289  fnasrn  6317  fliftf  6465  abrexex  7033  abrexexg  7034  fo1st  7079  fo2nd  7080  qliftf  7722  abrexfi  8149  iinfi  8206  tz9.12lem1  8533  infmap2  8923  cfslb2n  8973  fin23lem29  9046  fin23lem30  9047  fin1a2lem11  9115  ac6num  9184  rankcf  9478  tskuni  9484  negfi  10850  4sqlem11  15497  4sqlem12  15498  vdwapval  15515  vdwlem6  15528  quslem  16026  conjnmzb  17518  pmtrprfvalrn  17731  sylow1lem2  17837  sylow3lem1  17865  sylow3lem2  17866  rnascl  19164  ellspd  19960  iinopn  20532  restco  20778  pnrmopn  20957  cncmp  21005  discmp  21011  comppfsc  21145  alexsublem  21658  ptcmplem3  21668  snclseqg  21729  prdsxmetlem  21983  prdsbl  22106  xrhmeo  22553  pi1xfrf  22661  pi1cof  22667  iunmbl  23128  voliun  23129  itg1addlem4  23272  i1fmulc  23276  mbfi1fseqlem4  23291  itg2monolem1  23323  aannenlem2  23888  2lgslem1b  24917  mptelee  25575  nbgraf1olem5  25974  fargshiftfo  26166  disjrnmpt  28780  ofrn2  28822  abrexct  28882  abrexctf  28884  esumc  29440  esumrnmpt  29441  carsgclctunlem3  29709  eulerpartlemt  29760  bdayfo  31074  fobigcup  31177  ptrest  32578  areacirclem2  32671  istotbnd3  32740  sstotbnd  32744  rmxypairf1o  36494  hbtlem6  36718  elrnmptf  38362  fnrnafv  39891