Theorem rnmpt 5921

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 5918	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5189	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2752	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5901	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3054	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2796	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2762	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707  ∃wrex 3053  {copab 5169   ↦ cmpt 5188  ran crn 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  elrnmpt  5922  elrnmpt1  5924  elrnmptg  5925  dfiun3g  5931  dfiin3g  5932  fnrnfv  6920  fmpt  7082  fnasrn  7117  fliftf  7290  abrexexgOLD  7940  fo1st  7988  fo2nd  7989  fsplitfpar  8097  qliftf  8778  abrexfi  9303  iinfi  9368  tz9.12lem1  9740  infmap2  10170  cfslb2n  10221  fin23lem29  10294  fin23lem30  10295  fin1a2lem11  10363  ac6num  10432  rankcf  10730  tskuni  10736  negfi  12132  4sqlem11  16926  4sqlem12  16927  vdwapval  16944  vdwlem6  16957  quslem  17506  smndex2dnrinv  18842  conjnmzb  19185  pmtrprfvalrn  19418  sylow1lem2  19529  sylow3lem1  19557  sylow3lem2  19558  ablsimpgfind  20042  pzriprnglem10  21400  ellspd  21711  rnascl  21800  iinopn  22789  restco  23051  pnrmopn  23230  cncmp  23279  discmp  23285  comppfsc  23419  alexsublem  23931  ptcmplem3  23941  snclseqg  24003  prdsxmetlem  24256  prdsbl  24379  xrhmeo  24844  pi1xfrf  24953  pi1cof  24959  iunmbl  25454  voliun  25455  itg1addlem4  25600  i1fmulc  25604  mbfi1fseqlem4  25619  itg2monolem1  25651  aannenlem2  26237  2lgslem1b  27303  bdayfo  27589  nosupno  27615  noinfno  27630  addsuniflem  27908  mptelee  28822  disjrnmpt  32514  ofrn2  32564  abrexct  32640  abrexctf  32642  qusbas2  33377  nsgqusf1olem2  33385  esumc  34041  esumrnmpt  34042  carsgclctunlem3  34311  eulerpartlemt  34362  fobigcup  35888  ptrest  37613  areacirclem2  37703  istotbnd3  37765  sstotbnd  37769  dfqs2  42225  rnasclg  42487  rmxypairf1o  42900  hbtlem6  43118  onsucrn  43260  elrnmptf  45175  fnrnafv  47163  fundcmpsurinjlem1  47399  imasetpreimafvbijlemfo  47406  fargshiftfo  47443