Theorem rnmpt 5947

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 5944	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5193	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2786	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5927	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3090	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2830	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2796	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  {cab 2741  ∃wrex 3089  {copab 5173   ↦ cmpt 5192  ran crn 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-mpt 5193  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  elrnmpt  5948  elrnmpt1  5950  elrnmptg  5951  dfiun3g  5958  dfiin3g  5959  fnrnfv  6940  fmpt  7105  fnasrn  7141  fliftf  7313  fo1st  8002  fo2nd  8003  fsplitfpar  8109  dfqs2  8697  qliftf  8799  abrexfi  9305  iinfi  9373  tz9.12lem1  9755  infmap2  10196  cfslb2n  10247  fin23lem29  10320  fin23lem30  10321  fin1a2lem11  10389  ac6num  10458  rankcf  10757  tskuni  10763  negfi  12159  4sqlem11  17010  4sqlem12  17011  vdwapval  17028  vdwlem6  17041  quslem  17592  smndex2dnrinv  18972  conjnmzb  19318  pmtrprfvalrn  19553  sylow1lem2  19664  sylow3lem1  19692  sylow3lem2  19693  ablsimpgfind  20177  pzriprnglem10  21640  ellspd  21952  rnascl  22041  iinopn  23059  restco  23321  pnrmopn  23500  cncmp  23549  discmp  23555  comppfsc  23689  alexsublem  24201  ptcmplem3  24211  snclseqg  24273  prdsxmetlem  24525  prdsbl  24648  xrhmeo  25105  pi1xfrf  25212  pi1cof  25218  iunmbl  25712  voliun  25713  itg1addlem4  25858  i1fmulc  25862  mbfi1fseqlem4  25877  itg2monolem1  25909  aannenlem2  26492  2lgslem1b  27556  bdayfo  27841  nosupno  27867  noinfno  27882  addsuniflem  28194  mpteleeOLD  29245  disjrnmpt  32930  ofrn2  32985  abrexct  33060  abrexctf  33062  qusbas2  33715  nsgqusf1olem2  33723  esumc  34441  esumrnmpt  34442  carsgclctunlem3  34710  eulerpartlemt  34761  vonf1oonfo  35599  fobigcup  36390  ptrest  38270  areacirclem2  38360  istotbnd3  38422  sstotbnd  38426  rnasclg  43273  rmxypairf1o  43638  hbtlem6  43856  onsucrn  43998  elrnmptf  45899  fnrnafv  47899  fundcmpsurinjlem1  48147  imasetpreimafvbijlemfo  48154  fargshiftfo  48191