Theorem rnmpt 5945

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 5942	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5191	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2785	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5925	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3089	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2829	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2795	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2740  ∃wrex 3088  {copab 5171   ↦ cmpt 5190  ran crn 5660

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 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-mpt 5191  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is used by:  elrnmpt  5946  elrnmpt1  5948  elrnmptg  5949  dfiun3g  5956  dfiin3g  5957  fnrnfv  6941  fmpt  7107  fnasrn  7145  fliftf  7320  fo1st  8010  fo2nd  8011  fsplitfpar  8119  dfqs2  8707  qliftf  8809  abrexfi  9323  iinfi  9391  tz9.12lem1  9773  infmap2  10223  cfslb2n  10274  fin23lem29  10347  fin23lem30  10348  fin1a2lem11  10416  ac6num  10485  rankcf  10790  tskuni  10796  negfi  12192  4sqlem11  17053  4sqlem12  17054  vdwapval  17071  vdwlem6  17084  quslem  17635  smndex2dnrinv  19033  conjnmzb  19386  pmtrprfvalrn  19621  sylow1lem2  19732  sylow3lem1  19760  sylow3lem2  19761  ablsimpgfind  20245  pzriprnglem10  21709  ellspd  22021  rnascl  22112  iinopn  23133  restco  23395  pnrmopn  23574  cncmp  23623  discmp  23629  abrexct  23686  comppfsc  23764  alexsublem  24276  ptcmplem3  24286  snclseqg  24348  prdsxmetlem  24600  prdsbl  24723  xrhmeo  25180  pi1xfrf  25287  pi1cof  25293  iunmbl  25787  voliun  25788  itg1addlem4  25933  i1fmulc  25937  mbfi1fseqlem4  25952  itg2monolem1  25984  aannenlem2  26572  2lgslem1b  27636  bdayfo  27921  nosupno  27947  noinfno  27962  addsuniflem  28274  mpteleeOLD  29360  disjrnmpt  33066  ofrn2  33121  abrexctf  33196  qusbas2  33843  nsgqusf1olem2  33851  esumc  34569  esumrnmpt  34570  carsgclctunlem3  34839  eulerpartlemt  34890  vonf1oonfo  35720  fobigcup  36485  ptrest  38376  areacirclem2  38466  istotbnd3  38529  sstotbnd  38533  rnasclg  43395  rmxypairf1o  43760  hbtlem6  43978  onsucrn  44120  elrnmptf  46021  omeiunle  47353  fnrnafv  48058  fundcmpsurinjlem1  48306  imasetpreimafvbijlemfo  48313  fargshiftfo  48350