Theorem rnmpt 5939

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 5936	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5187	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2784	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5919	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3088	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2828	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2794	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2739  ∃wrex 3087  {copab 5167   ↦ cmpt 5186  ran crn 5652

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 2733  ax-sep 5249  ax-pr 5391

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-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rex 3088  df-rab 3414  df-v 3453  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 5659  df-dm 5661  df-rn 5662

This theorem is used by:  elrnmpt  5940  elrnmpt1  5942  elrnmptg  5943  dfiun3g  5950  dfiin3g  5951  fnrnfv  6942  fmpt  7108  fnasrn  7146  fliftf  7321  fo1st  8019  fo2nd  8020  fsplitfpar  8127  dfqs2  8717  qliftf  8819  abrexfi  9334  iinfi  9402  tz9.12lem1  9787  infmap2  10288  cfslb2n  10339  fin23lem29  10412  fin23lem30  10413  fin1a2lem11  10481  ac6num  10550  rankcf  10855  tskuni  10861  negfi  12259  4sqlem11  17126  4sqlem12  17127  vdwapval  17144  vdwlem6  17157  quslem  17708  smndex2dnrinv  19107  conjnmzb  19460  pmtrprfvalrn  19695  sylow1lem2  19806  sylow3lem1  19834  sylow3lem2  19835  ablsimpgfind  20319  pzriprnglem10  21789  ellspd  22101  rnascl  22192  iinopn  23213  restco  23475  pnrmopn  23654  cncmp  23703  discmp  23709  abrexct  23766  comppfsc  23844  alexsublem  24356  ptcmplem3  24366  snclseqg  24428  prdsxmetlem  24680  prdsbl  24803  xrhmeo  25260  pi1xfrf  25367  pi1cof  25373  iunmbl  25867  voliun  25868  itg1addlem4  26013  i1fmulc  26017  mbfi1fseqlem4  26032  itg2monolem1  26064  aannenlem2  26649  2lgslem1b  27712  bdayfo  28027  nosupno  28053  noinfno  28068  addsuniflem  28380  mpteleeOLD  29466  disjrnmpt  33172  ofrn2  33227  abrexctf  33302  qusbas2  33950  nsgqusf1olem2  33958  esumc  34676  esumrnmpt  34677  carsgclctunlem3  34945  eulerpartlemt  34996  vonf1oonfo  35877  fobigcup  36642  ptrest  38517  areacirclem2  38607  istotbnd3  38685  sstotbnd  38689  rnasclg  43543  rmxypairf1o  43897  hbtlem6  44115  onsucrn  44257  elrnmptf  46165  omeiunle  47496  fnrnafv  48201  fundcmpsurinjlem1  48449  imasetpreimafvbijlemfo  48456  fargshiftfo  48493