Theorem rnmpt 5791

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 5790	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5111	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2821	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5771	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3112	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2863	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2831	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  ∃wrex 3107  {copab 5092   ↦ cmpt 5110  ran crn 5520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-mpt 5111  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  elrnmpt  5792  elrnmpt1  5794  elrnmptg  5795  dfiun3g  5800  dfiin3g  5801  fnrnfv  6700  fmpt  6851  fnasrn  6884  fliftf  7047  abrexexg  7644  fo1st  7691  fo2nd  7692  fsplitfpar  7797  qliftf  8368  abrexfi  8808  iinfi  8865  tz9.12lem1  9200  infmap2  9629  cfslb2n  9679  fin23lem29  9752  fin23lem30  9753  fin1a2lem11  9821  ac6num  9890  rankcf  10188  tskuni  10194  negfi  11577  4sqlem11  16281  4sqlem12  16282  vdwapval  16299  vdwlem6  16312  quslem  16808  smndex2dnrinv  18072  conjnmzb  18385  pmtrprfvalrn  18608  sylow1lem2  18716  sylow3lem1  18744  sylow3lem2  18745  ablsimpgfind  19225  ellspd  20491  rnascl  20577  iinopn  21507  restco  21769  pnrmopn  21948  cncmp  21997  discmp  22003  comppfsc  22137  alexsublem  22649  ptcmplem3  22659  snclseqg  22721  prdsxmetlem  22975  prdsbl  23098  xrhmeo  23551  pi1xfrf  23658  pi1cof  23664  iunmbl  24157  voliun  24158  itg1addlem4  24303  i1fmulc  24307  mbfi1fseqlem4  24322  itg2monolem1  24354  aannenlem2  24925  2lgslem1b  25976  mptelee  26689  disjrnmpt  30348  ofrn2  30401  abrexct  30478  abrexctf  30480  esumc  31420  esumrnmpt  31421  carsgclctunlem3  31688  eulerpartlemt  31739  bdayfo  33295  nosupno  33316  fobigcup  33474  ptrest  35056  areacirclem2  35146  istotbnd3  35209  sstotbnd  35213  dfqs2  39417  rnasclg  39426  rmxypairf1o  39852  hbtlem6  40073  elrnmptf  41807  fnrnafv  43718  fundcmpsurinjlem1  43915  imasetpreimafvbijlemfo  43922  fargshiftfo  43959