Theorem rnmpt 5942

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 5939	. 2 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
2		rnmpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3		df-mpt 5207	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	2, 3	eqtri 2759	. . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5	4	rneqi 5922	. 2 ⊢ ran 𝐹 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6		df-rex 3062	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
7	6	abbii 2803	. 2 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
8	1, 5, 7	3eqtr4i 2769	1 ⊢ ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵}

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2714  ∃wrex 3061  {copab 5186   ↦ cmpt 5206  ran crn 5660

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-mpt 5207  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  elrnmpt  5943  elrnmpt1  5945  elrnmptg  5946  dfiun3g  5952  dfiin3g  5953  fnrnfv  6943  fmpt  7105  fnasrn  7140  fliftf  7313  abrexexgOLD  7965  fo1st  8013  fo2nd  8014  fsplitfpar  8122  qliftf  8824  abrexfi  9369  iinfi  9434  tz9.12lem1  9806  infmap2  10236  cfslb2n  10287  fin23lem29  10360  fin23lem30  10361  fin1a2lem11  10429  ac6num  10498  rankcf  10796  tskuni  10802  negfi  12196  4sqlem11  16980  4sqlem12  16981  vdwapval  16998  vdwlem6  17011  quslem  17562  smndex2dnrinv  18898  conjnmzb  19241  pmtrprfvalrn  19474  sylow1lem2  19585  sylow3lem1  19613  sylow3lem2  19614  ablsimpgfind  20098  pzriprnglem10  21456  ellspd  21767  rnascl  21856  iinopn  22845  restco  23107  pnrmopn  23286  cncmp  23335  discmp  23341  comppfsc  23475  alexsublem  23987  ptcmplem3  23997  snclseqg  24059  prdsxmetlem  24312  prdsbl  24435  xrhmeo  24900  pi1xfrf  25009  pi1cof  25015  iunmbl  25511  voliun  25512  itg1addlem4  25657  i1fmulc  25661  mbfi1fseqlem4  25676  itg2monolem1  25708  aannenlem2  26294  2lgslem1b  27360  bdayfo  27646  nosupno  27672  noinfno  27687  addsuniflem  27965  mptelee  28879  disjrnmpt  32571  ofrn2  32623  abrexct  32699  abrexctf  32701  qusbas2  33426  nsgqusf1olem2  33434  esumc  34087  esumrnmpt  34088  carsgclctunlem3  34357  eulerpartlemt  34408  fobigcup  35923  ptrest  37648  areacirclem2  37738  istotbnd3  37800  sstotbnd  37804  dfqs2  42255  rnasclg  42489  rmxypairf1o  42902  hbtlem6  43120  onsucrn  43262  elrnmptf  45172  fnrnafv  47158  fundcmpsurinjlem1  47379  imasetpreimafvbijlemfo  47386  fargshiftfo  47423