Theorem rnmpt 5904

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 5901	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5178	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2757	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5884	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3059	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2801	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2767	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  {cab 2712  ∃wrex 3058  {copab 5158   ↦ cmpt 5177  ran crn 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-mpt 5178  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  elrnmpt  5905  elrnmpt1  5907  elrnmptg  5908  dfiun3g  5915  dfiin3g  5916  fnrnfv  6891  fmpt  7053  fnasrn  7088  fliftf  7259  fo1st  7951  fo2nd  7952  fsplitfpar  8058  qliftf  8740  abrexfi  9250  iinfi  9318  tz9.12lem1  9697  infmap2  10125  cfslb2n  10176  fin23lem29  10249  fin23lem30  10250  fin1a2lem11  10318  ac6num  10387  rankcf  10686  tskuni  10692  negfi  12089  4sqlem11  16881  4sqlem12  16882  vdwapval  16899  vdwlem6  16912  quslem  17462  smndex2dnrinv  18838  conjnmzb  19180  pmtrprfvalrn  19415  sylow1lem2  19526  sylow3lem1  19554  sylow3lem2  19555  ablsimpgfind  20039  pzriprnglem10  21443  ellspd  21755  rnascl  21845  iinopn  22844  restco  23106  pnrmopn  23285  cncmp  23334  discmp  23340  comppfsc  23474  alexsublem  23986  ptcmplem3  23996  snclseqg  24058  prdsxmetlem  24310  prdsbl  24433  xrhmeo  24898  pi1xfrf  25007  pi1cof  25013  iunmbl  25508  voliun  25509  itg1addlem4  25654  i1fmulc  25658  mbfi1fseqlem4  25673  itg2monolem1  25705  aannenlem2  26291  2lgslem1b  27357  bdayfo  27643  nosupno  27669  noinfno  27684  addsuniflem  27971  mpteleeOLD  28917  disjrnmpt  32609  ofrn2  32667  abrexct  32743  abrexctf  32745  qusbas2  33436  nsgqusf1olem2  33444  esumc  34157  esumrnmpt  34158  carsgclctunlem3  34426  eulerpartlemt  34477  fobigcup  36041  ptrest  37759  areacirclem2  37849  istotbnd3  37911  sstotbnd  37915  dfqs2  42435  rnasclg  42696  rmxypairf1o  43095  hbtlem6  43313  onsucrn  43455  elrnmptf  45367  fnrnafv  47350  fundcmpsurinjlem1  47586  imasetpreimafvbijlemfo  47593  fargshiftfo  47630