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

Theorem dmmptg 5340
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 2986 . . . 4  |-  ( B  e.  V  ->  B  e.  _V )
21ralimi 2796 . . 3  |-  ( A. x  e.  A  B  e.  V  ->  A. x  e.  A  B  e.  _V )
3 rabid2 2903 . . 3  |-  ( A  =  { x  e.  A  |  B  e. 
_V }  <->  A. x  e.  A  B  e.  _V )
42, 3sylibr 212 . 2  |-  ( A. x  e.  A  B  e.  V  ->  A  =  { x  e.  A  |  B  e.  _V } )
5 eqid 2443 . . 3  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
65dmmpt 5338 . 2  |-  dom  (
x  e.  A  |->  B )  =  { x  e.  A  |  B  e.  _V }
74, 6syl6reqr 2494 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 1369    e. wcel 1756   A.wral 2720   {crab 2724   _Vcvv 2977    e. cmpt 4355   dom cdm 4845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-br 4298  df-opab 4356  df-mpt 4357  df-xp 4851  df-rel 4852  df-cnv 4853  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858
This theorem is referenced by:  suppssov1  6726  suppssfv  6730  iinon  6806  onoviun  6809  noinfep  7870  cantnfdm  7875  cantnfdmOLD  7877  axcc2lem  8610  o1lo1  13020  o1lo12  13021  lo1mptrcl  13104  o1mptrcl  13105  o1add2  13106  o1mul2  13107  o1sub2  13108  lo1add  13109  lo1mul  13110  o1dif  13112  rlimneg  13129  lo1le  13134  rlimno1  13136  o1fsum  13281  divsfval  14490  iscnp2  18848  ptcnplem  19199  xkoinjcn  19265  fbasrn  19462  prdsdsf  19947  ressprdsds  19951  mbfmptcl  21120  mbfdm2  21121  dvmptcl  21438  dvmptadd  21439  dvmptmul  21440  dvmptres2  21441  dvmptcmul  21443  dvmptcj  21447  dvmptco  21451  rolle  21467  dvlip  21470  dvlipcn  21471  dvle  21484  dvivthlem1  21485  dvivth  21487  dvfsumle  21498  dvfsumge  21499  dvmptrecl  21501  dvfsumlem2  21504  pserdv  21899  logtayl  22110  rlimcxp  22372  o1cxp  22373  gsummpt2co  26254  measdivcstOLD  26643  probfinmeasbOLD  26816  probmeasb  26818  dstrvprob  26859  cvmsss2  27168  sdclem2  28643  dmmzp  29074  stoweidlem27  29827  ovmpt3rabdm  30167
  Copyright terms: Public domain W3C validator