Theorem rnmpt 5941

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 5938	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5187	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2783	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5921	. 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 1570  ∃wex 1812   ∈ wcel 2145  {cab 2738  ∃wrex 3086  {copab 5167   ↦ cmpt 5186  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  elrnmpt  5942  elrnmpt1  5944  elrnmptg  5945  dfiun3g  5952  dfiin3g  5953  fnrnfv  6937  fmpt  7103  fnasrn  7141  fliftf  7316  fo1st  8006  fo2nd  8007  fsplitfpar  8115  dfqs2  8703  qliftf  8805  abrexfi  9319  iinfi  9387  tz9.12lem1  9769  infmap2  10219  cfslb2n  10270  fin23lem29  10343  fin23lem30  10344  fin1a2lem11  10412  ac6num  10481  rankcf  10786  tskuni  10792  negfi  12188  4sqlem11  17047  4sqlem12  17048  vdwapval  17065  vdwlem6  17078  quslem  17629  smndex2dnrinv  19027  conjnmzb  19380  pmtrprfvalrn  19615  sylow1lem2  19726  sylow3lem1  19754  sylow3lem2  19755  ablsimpgfind  20239  pzriprnglem10  21703  ellspd  22015  rnascl  22106  iinopn  23127  restco  23389  pnrmopn  23568  cncmp  23617  discmp  23623  abrexct  23680  comppfsc  23758  alexsublem  24270  ptcmplem3  24280  snclseqg  24342  prdsxmetlem  24594  prdsbl  24717  xrhmeo  25174  pi1xfrf  25281  pi1cof  25287  iunmbl  25781  voliun  25782  itg1addlem4  25927  i1fmulc  25931  mbfi1fseqlem4  25946  itg2monolem1  25978  aannenlem2  26565  2lgslem1b  27628  bdayfo  27913  nosupno  27939  noinfno  27954  addsuniflem  28266  mpteleeOLD  29352  disjrnmpt  33058  ofrn2  33113  abrexctf  33188  qusbas2  33835  nsgqusf1olem2  33843  esumc  34561  esumrnmpt  34562  carsgclctunlem3  34831  eulerpartlemt  34882  vonf1oonfo  35712  fobigcup  36477  ptrest  38368  areacirclem2  38458  istotbnd3  38521  sstotbnd  38525  rnasclg  43387  rmxypairf1o  43752  hbtlem6  43970  onsucrn  44112  elrnmptf  46013  omeiunle  47345  fnrnafv  48050  fundcmpsurinjlem1  48298  imasetpreimafvbijlemfo  48305  fargshiftfo  48342