MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmmpt Structured version   Visualization version   GIF version

Theorem dmmpt 6154
Description: The domain of the mapping operation in general. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.)
Hypothesis
Ref Expression
dmmpt.1 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
dmmpt dom 𝐹 = {𝑥𝐴𝐵 ∈ V}

Proof of Theorem dmmpt
StepHypRef Expression
1 dfdm4 5813 . 2 dom 𝐹 = ran 𝐹
2 dfrn4 6116 . 2 ran 𝐹 = (𝐹 “ V)
3 dmmpt.1 . . 3 𝐹 = (𝑥𝐴𝐵)
43mptpreima 6152 . 2 (𝐹 “ V) = {𝑥𝐴𝐵 ∈ V}
51, 2, 43eqtri 2768 1 dom 𝐹 = {𝑥𝐴𝐵 ∈ V}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  wcel 2104  {crab 3284  Vcvv 3437  cmpt 5164  ccnv 5595  dom cdm 5596  ran crn 5597  cima 5599
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-mpt 5165  df-xp 5602  df-rel 5603  df-cnv 5604  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609
This theorem is referenced by:  dmmptss  6155  dmmptg  6156  dmmptd  6604  fvmpti  6902  fvmptss  6915  fvmptss2  6928  mptexgf  7126  tz9.12lem3  9587  cardf2  9741  pmtrsn  19168  00lsp  20284  rgrx0ndm  28001  abrexexd  30895  funcnvmpt  31045  mptctf  31093  issibf  32341  rdgprc0  33810  imageval  34273  dmmptdff  42806  dmmptssf  42819  dmmptdf2  42820  dvcosre  43501  itgsinexplem1  43543  stirlinglem14  43676  fvmptrabdm  44842
  Copyright terms: Public domain W3C validator