Theorem rnmpt 5670

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 5669	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5009	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2802	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5650	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3094	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2844	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2812	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 387   = wceq 1507  ∃wex 1742   ∈ wcel 2050  {cab 2758  ∃wrex 3089  {copab 4991   ↦ cmpt 5008  ran crn 5408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930  df-opab 4992  df-mpt 5009  df-cnv 5415  df-dm 5417  df-rn 5418

This theorem is referenced by:  elrnmpt  5671  elrnmpt1  5673  elrnmptg  5674  dfiun3g  5677  dfiin3g  5678  fnrnfv  6555  fmpt  6697  fnasrn  6730  fliftf  6891  abrexexg  7474  fo1st  7521  fo2nd  7522  qliftf  8185  abrexfi  8619  iinfi  8676  tz9.12lem1  9010  infmap2  9438  cfslb2n  9488  fin23lem29  9561  fin23lem30  9562  fin1a2lem11  9630  ac6num  9699  rankcf  9997  tskuni  10003  negfi  11390  4sqlem11  16147  4sqlem12  16148  vdwapval  16165  vdwlem6  16178  quslem  16672  conjnmzb  18164  pmtrprfvalrn  18377  sylow1lem2  18485  sylow3lem1  18513  sylow3lem2  18514  rnascl  19837  ellspd  20648  iinopn  21214  restco  21476  pnrmopn  21655  cncmp  21704  discmp  21710  comppfsc  21844  alexsublem  22356  ptcmplem3  22366  snclseqg  22427  prdsxmetlem  22681  prdsbl  22804  xrhmeo  23253  pi1xfrf  23360  pi1cof  23366  iunmbl  23857  voliun  23858  itg1addlem4  24003  i1fmulc  24007  mbfi1fseqlem4  24022  itg2monolem1  24054  aannenlem2  24621  2lgslem1b  25670  mptelee  26384  disjrnmpt  30101  ofrn2  30149  abrexct  30211  abrexctf  30213  esumc  30960  esumrnmpt  30961  carsgclctunlem3  31229  eulerpartlemt  31280  bdayfo  32709  nosupno  32730  fobigcup  32888  ptrest  34338  areacirclem2  34430  istotbnd3  34497  sstotbnd  34501  dfqs2  38573  rmxypairf1o  38910  hbtlem6  39131  ablsimpgfind  40051  elrnmptf  40871  fnrnafv  42773  fargshiftfo  42980