Theorem rnmpt 5924

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 5921	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5192	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2753	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5904	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3055	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2797	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2763	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2708  ∃wrex 3054  {copab 5172   ↦ cmpt 5191  ran crn 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-cnv 5649  df-dm 5651  df-rn 5652

This theorem is referenced by:  elrnmpt  5925  elrnmpt1  5927  elrnmptg  5928  dfiun3g  5934  dfiin3g  5935  fnrnfv  6923  fmpt  7085  fnasrn  7120  fliftf  7293  abrexexgOLD  7943  fo1st  7991  fo2nd  7992  fsplitfpar  8100  qliftf  8781  abrexfi  9310  iinfi  9375  tz9.12lem1  9747  infmap2  10177  cfslb2n  10228  fin23lem29  10301  fin23lem30  10302  fin1a2lem11  10370  ac6num  10439  rankcf  10737  tskuni  10743  negfi  12139  4sqlem11  16933  4sqlem12  16934  vdwapval  16951  vdwlem6  16964  quslem  17513  smndex2dnrinv  18849  conjnmzb  19192  pmtrprfvalrn  19425  sylow1lem2  19536  sylow3lem1  19564  sylow3lem2  19565  ablsimpgfind  20049  pzriprnglem10  21407  ellspd  21718  rnascl  21807  iinopn  22796  restco  23058  pnrmopn  23237  cncmp  23286  discmp  23292  comppfsc  23426  alexsublem  23938  ptcmplem3  23948  snclseqg  24010  prdsxmetlem  24263  prdsbl  24386  xrhmeo  24851  pi1xfrf  24960  pi1cof  24966  iunmbl  25461  voliun  25462  itg1addlem4  25607  i1fmulc  25611  mbfi1fseqlem4  25626  itg2monolem1  25658  aannenlem2  26244  2lgslem1b  27310  bdayfo  27596  nosupno  27622  noinfno  27637  addsuniflem  27915  mptelee  28829  disjrnmpt  32521  ofrn2  32571  abrexct  32647  abrexctf  32649  qusbas2  33384  nsgqusf1olem2  33392  esumc  34048  esumrnmpt  34049  carsgclctunlem3  34318  eulerpartlemt  34369  fobigcup  35895  ptrest  37620  areacirclem2  37710  istotbnd3  37772  sstotbnd  37776  dfqs2  42232  rnasclg  42494  rmxypairf1o  42907  hbtlem6  43125  onsucrn  43267  elrnmptf  45182  fnrnafv  47167  fundcmpsurinjlem1  47403  imasetpreimafvbijlemfo  47410  fargshiftfo  47447