MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmmptg Structured version   Unicode version

Theorem dmmptg 5322
Description: The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.)
Assertion
Ref Expression
dmmptg  |-  ( A. x  e.  A  B  e.  V  ->  dom  (
x  e.  A  |->  B )  =  A )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    V( x)

Proof of Theorem dmmptg
StepHypRef Expression
1 elex 3070 . . . 4  |-  ( B  e.  V  ->  B  e.  _V )
21ralimi 2799 . . 3  |-  ( A. x  e.  A  B  e.  V  ->  A. x  e.  A  B  e.  _V )
3 rabid2 2987 . . 3  |-  ( A  =  { x  e.  A  |  B  e. 
_V }  <->  A. x  e.  A  B  e.  _V )
42, 3sylibr 214 . 2  |-  ( A. x  e.  A  B  e.  V  ->  A  =  { x  e.  A  |  B  e.  _V } )
5 eqid 2404 . . 3  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
65dmmpt 5320 . 2  |-  dom  (
x  e.  A  |->  B )  =  { x  e.  A  |  B  e.  _V }
74, 6syl6reqr 2464 1  |-  ( A. x  e.  A  B  e.  V  ->  dom  (
x  e.  A  |->  B )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1407    e. wcel 1844   A.wral 2756   {crab 2760   _Vcvv 3061    |-> cmpt 4455   dom cdm 4825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pr 4632
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-br 4398  df-opab 4456  df-mpt 4457  df-xp 4831  df-rel 4832  df-cnv 4833  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838
This theorem is referenced by:  ovmpt3rabdm  6518  suppssov1  6937  suppssfv  6941  iinon  7046  onoviun  7049  noinfep  8111  cantnfdm  8115  cantnfdmOLD  8117  axcc2lem  8850  swrd0  12717  o1lo1  13511  o1lo12  13512  lo1mptrcl  13595  o1mptrcl  13596  o1add2  13597  o1mul2  13598  o1sub2  13599  lo1add  13600  lo1mul  13601  o1dif  13603  rlimneg  13620  lo1le  13625  rlimno1  13627  o1fsum  13780  divsfval  15163  iscnp2  20035  ptcnplem  20416  xkoinjcn  20482  fbasrn  20679  prdsdsf  21164  ressprdsds  21168  mbfmptcl  22338  mbfdm2  22339  dvmptcl  22656  dvmptadd  22657  dvmptmul  22658  dvmptres2  22659  dvmptcmul  22661  dvmptcj  22665  dvmptco  22669  rolle  22685  dvlip  22688  dvlipcn  22689  dvle  22702  dvivthlem1  22703  dvivth  22705  dvfsumle  22716  dvfsumge  22717  dvmptrecl  22719  dvfsumlem2  22722  pserdv  23118  logtayl  23337  relogbf  23460  rlimcxp  23631  o1cxp  23632  gsummpt2co  28235  measdivcstOLD  28685  probfinmeasbOLD  28886  probmeasb  28888  dstrvprob  28929  cvmsss2  29584  sdclem2  31530  dmmzp  35040  dvmptresicc  37097  dvcosax  37104  dvnprodlem3  37126  itgcoscmulx  37149  stoweidlem27  37190  dirkeritg  37265  fourierdlem16  37286  fourierdlem21  37291  fourierdlem22  37292  fourierdlem39  37309  fourierdlem57  37327  fourierdlem58  37328  fourierdlem60  37330  fourierdlem61  37331  fourierdlem73  37343  fourierdlem83  37353  elbigofrcl  38694
  Copyright terms: Public domain W3C validator