Theorem rnmpt 5371

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 5370	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 4730	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2644	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5352	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 2918	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2739	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2654	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  {cab 2608  ∃wrex 2913  {copab 4712   ↦ cmpt 4729  ran crn 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-mpt 4730  df-cnv 5122  df-dm 5124  df-rn 5125

This theorem is referenced by:  elrnmpt  5372  elrnmpt1  5374  elrnmptg  5375  dfiun3g  5378  dfiin3g  5379  fnrnfv  6242  fmpt  6381  fnasrn  6411  fliftf  6565  abrexexg  7140  abrexexOLD  7142  fo1st  7188  fo2nd  7189  qliftf  7835  abrexfi  8266  iinfi  8323  tz9.12lem1  8650  infmap2  9040  cfslb2n  9090  fin23lem29  9163  fin23lem30  9164  fin1a2lem11  9232  ac6num  9301  rankcf  9599  tskuni  9605  negfi  10971  4sqlem11  15659  4sqlem12  15660  vdwapval  15677  vdwlem6  15690  quslem  16203  conjnmzb  17695  pmtrprfvalrn  17908  sylow1lem2  18014  sylow3lem1  18042  sylow3lem2  18043  rnascl  19343  ellspd  20141  iinopn  20707  restco  20968  pnrmopn  21147  cncmp  21195  discmp  21201  comppfsc  21335  alexsublem  21848  ptcmplem3  21858  snclseqg  21919  prdsxmetlem  22173  prdsbl  22296  xrhmeo  22745  pi1xfrf  22853  pi1cof  22859  iunmbl  23321  voliun  23322  itg1addlem4  23466  i1fmulc  23470  mbfi1fseqlem4  23485  itg2monolem1  23517  aannenlem2  24084  2lgslem1b  25117  mptelee  25775  disjrnmpt  29398  ofrn2  29442  abrexct  29494  abrexctf  29496  esumc  30113  esumrnmpt  30114  carsgclctunlem3  30382  eulerpartlemt  30433  bdayfo  31828  nosupno  31849  fobigcup  32007  ptrest  33408  areacirclem2  33501  istotbnd3  33570  sstotbnd  33574  rmxypairf1o  37476  hbtlem6  37699  elrnmptf  39367  fnrnafv  41242  fargshiftfo  41378