Theorem rnmpt 5949

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 5946	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5195	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2788	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5929	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3092	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2832	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2798	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  {cab 2743  ∃wrex 3091  {copab 5175   ↦ cmpt 5194  ran crn 5664

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by:  elrnmpt  5950  elrnmpt1  5952  elrnmptg  5953  dfiun3g  5960  dfiin3g  5961  fnrnfv  6944  fmpt  7109  fnasrn  7147  fliftf  7322  fo1st  8012  fo2nd  8013  fsplitfpar  8119  dfqs2  8707  qliftf  8809  abrexfi  9316  iinfi  9384  tz9.12lem1  9766  infmap2  10216  cfslb2n  10267  fin23lem29  10340  fin23lem30  10341  fin1a2lem11  10409  ac6num  10478  rankcf  10777  tskuni  10783  negfi  12179  4sqlem11  17037  4sqlem12  17038  vdwapval  17055  vdwlem6  17068  quslem  17619  smndex2dnrinv  19014  conjnmzb  19367  pmtrprfvalrn  19602  sylow1lem2  19713  sylow3lem1  19741  sylow3lem2  19742  ablsimpgfind  20226  pzriprnglem10  21690  ellspd  22002  rnascl  22091  iinopn  23109  restco  23371  pnrmopn  23550  cncmp  23599  discmp  23605  abrexct  23662  comppfsc  23740  alexsublem  24252  ptcmplem3  24262  snclseqg  24324  prdsxmetlem  24576  prdsbl  24699  xrhmeo  25156  pi1xfrf  25263  pi1cof  25269  iunmbl  25763  voliun  25764  itg1addlem4  25909  i1fmulc  25913  mbfi1fseqlem4  25928  itg2monolem1  25960  aannenlem2  26543  2lgslem1b  27607  bdayfo  27892  nosupno  27918  noinfno  27933  addsuniflem  28245  mpteleeOLD  29300  disjrnmpt  33001  ofrn2  33056  abrexctf  33132  qusbas2  33779  nsgqusf1olem2  33787  esumc  34505  esumrnmpt  34506  carsgclctunlem3  34775  eulerpartlemt  34826  vonf1oonfo  35656  fobigcup  36427  ptrest  38327  areacirclem2  38417  istotbnd3  38480  sstotbnd  38484  rnasclg  43331  rmxypairf1o  43696  hbtlem6  43914  onsucrn  44056  elrnmptf  45957  omeiunle  47289  fnrnafv  47957  fundcmpsurinjlem1  48205  imasetpreimafvbijlemfo  48212  fargshiftfo  48249