Theorem rnmpt 5940

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 5937	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5186	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2783	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5920	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3087	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2827	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2793	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738  ∃wrex 3086  {copab 5166   ↦ cmpt 5185  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-mpt 5186  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  elrnmpt  5941  elrnmpt1  5943  elrnmptg  5944  dfiun3g  5951  dfiin3g  5952  fnrnfv  6949  fmpt  7115  fnasrn  7153  fliftf  7327  fo1st  8025  fo2nd  8026  fsplitfpar  8135  dfqs2  8731  qliftf  8833  abrexfi  9348  iinfi  9416  tz9.12lem1  9801  infmap2  10302  cfslb2n  10353  fin23lem29  10426  fin23lem30  10427  fin1a2lem11  10495  ac6num  10564  rankcf  10869  tskuni  10875  negfi  12273  4sqlem11  17142  4sqlem12  17143  vdwapval  17160  vdwlem6  17173  quslem  17724  smndex2dnrinv  19123  conjnmzb  19476  pmtrprfvalrn  19711  sylow1lem2  19822  sylow3lem1  19850  sylow3lem2  19851  ablsimpgfind  20335  pzriprnglem10  21805  ellspd  22117  rnascl  22208  iinopn  23229  restco  23491  pnrmopn  23670  cncmp  23719  discmp  23725  abrexct  23782  comppfsc  23860  alexsublem  24372  ptcmplem3  24382  snclseqg  24444  prdsxmetlem  24696  prdsbl  24819  xrhmeo  25276  pi1xfrf  25383  pi1cof  25389  iunmbl  25883  voliun  25884  itg1addlem4  26029  i1fmulc  26033  mbfi1fseqlem4  26048  itg2monolem1  26080  aannenlem2  26665  2lgslem1b  27728  bdayfo  28043  nosupno  28069  noinfno  28084  addsuniflem  28396  mpteleeOLD  29482  disjrnmpt  33230  ofrn2  33285  abrexctf  33360  qusbas2  34007  nsgqusf1olem2  34015  esumc  34733  esumrnmpt  34734  carsgclctunlem3  35002  eulerpartlemt  35053  vonf1oonfo  35972  fobigcup  36758  ptrest  38646  areacirclem2  38736  istotbnd3  38814  sstotbnd  38818  rnasclg  43672  rmxypairf1o  44027  hbtlem6  44240  onsucrn  44382  elrnmptf  46304  omeiunle  47635  fnrnafv  48340  fundcmpsurinjlem1  48588  imasetpreimafvbijlemfo  48595  fargshiftfo  48632