Theorem rnmpt 5912

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 5909	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5167	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2759	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5892	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3062	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2803	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2769	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2714  ∃wrex 3061  {copab 5147   ↦ cmpt 5166  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  elrnmpt  5913  elrnmpt1  5915  elrnmptg  5916  dfiun3g  5923  dfiin3g  5924  fnrnfv  6899  fmpt  7062  fnasrn  7098  fliftf  7270  fo1st  7962  fo2nd  7963  fsplitfpar  8068  dfqs2  8650  qliftf  8752  abrexfi  9262  iinfi  9330  tz9.12lem1  9711  infmap2  10139  cfslb2n  10190  fin23lem29  10263  fin23lem30  10264  fin1a2lem11  10332  ac6num  10401  rankcf  10700  tskuni  10706  negfi  12105  4sqlem11  16926  4sqlem12  16927  vdwapval  16944  vdwlem6  16957  quslem  17507  smndex2dnrinv  18886  conjnmzb  19228  pmtrprfvalrn  19463  sylow1lem2  19574  sylow3lem1  19602  sylow3lem2  19603  ablsimpgfind  20087  pzriprnglem10  21470  ellspd  21782  rnascl  21871  iinopn  22867  restco  23129  pnrmopn  23308  cncmp  23357  discmp  23363  comppfsc  23497  alexsublem  24009  ptcmplem3  24019  snclseqg  24081  prdsxmetlem  24333  prdsbl  24456  xrhmeo  24913  pi1xfrf  25020  pi1cof  25026  iunmbl  25520  voliun  25521  itg1addlem4  25666  i1fmulc  25670  mbfi1fseqlem4  25685  itg2monolem1  25717  aannenlem2  26295  2lgslem1b  27355  bdayfo  27641  nosupno  27667  noinfno  27682  addsuniflem  27993  mpteleeOLD  28964  disjrnmpt  32655  ofrn2  32713  abrexct  32788  abrexctf  32790  qusbas2  33466  nsgqusf1olem2  33474  esumc  34195  esumrnmpt  34196  carsgclctunlem3  34464  eulerpartlemt  34515  fobigcup  36080  ptrest  37940  areacirclem2  38030  istotbnd3  38092  sstotbnd  38096  rnasclg  42944  rmxypairf1o  43339  hbtlem6  43557  onsucrn  43699  elrnmptf  45611  fnrnafv  47610  fundcmpsurinjlem1  47858  imasetpreimafvbijlemfo  47865  fargshiftfo  47902