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

Theorem dmmptg 6099
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 (∀𝑥𝐴 𝐵𝑉 → dom (𝑥𝐴𝐵) = 𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem dmmptg
StepHypRef Expression
1 elex 3515 . . . 4 (𝐵𝑉𝐵 ∈ V)
21ralimi 3163 . . 3 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
3 rabid2 3384 . . 3 (𝐴 = {𝑥𝐴𝐵 ∈ V} ↔ ∀𝑥𝐴 𝐵 ∈ V)
42, 3sylibr 236 . 2 (∀𝑥𝐴 𝐵𝑉𝐴 = {𝑥𝐴𝐵 ∈ V})
5 eqid 2824 . . 3 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
65dmmpt 6097 . 2 dom (𝑥𝐴𝐵) = {𝑥𝐴𝐵 ∈ V}
74, 6syl6reqr 2878 1 (∀𝑥𝐴 𝐵𝑉 → dom (𝑥𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1536  wcel 2113  wral 3141  {crab 3145  Vcvv 3497  cmpt 5149  dom cdm 5558
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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-br 5070  df-opab 5132  df-mpt 5150  df-xp 5564  df-rel 5565  df-cnv 5566  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571
This theorem is referenced by:  ovmpt3rabdm  7407  suppssov1  7865  suppssfv  7869  iinon  7980  onoviun  7983  noinfep  9126  cantnfdm  9130  axcc2lem  9861  negfi  11592  ccatalpha  13950  swrd0  14023  o1lo1  14897  o1lo12  14898  lo1mptrcl  14981  o1mptrcl  14982  o1add2  14983  o1mul2  14984  o1sub2  14985  lo1add  14986  lo1mul  14987  o1dif  14989  rlimneg  15006  lo1le  15011  rlimno1  15013  o1fsum  15171  divsfval  16823  subdrgint  19585  iscnp2  21850  ptcnplem  22232  xkoinjcn  22298  fbasrn  22495  prdsdsf  22980  ressprdsds  22984  mbfmptcl  24240  mbfdm2  24241  dvmptcl  24559  dvmptadd  24560  dvmptmul  24561  dvmptres2  24562  dvmptcmul  24564  dvmptcj  24568  dvmptco  24572  rolle  24590  dvlip  24593  dvlipcn  24594  dvle  24607  dvivthlem1  24608  dvivth  24610  dvfsumle  24621  dvfsumge  24622  dvmptrecl  24624  dvfsumlem2  24627  pserdv  25020  logtayl  25246  relogbf  25372  rlimcxp  25554  o1cxp  25555  gsummpt2co  30690  psgnfzto1stlem  30746  measdivcstALTV  31488  probfinmeasbALTV  31691  probmeasb  31692  dstrvprob  31733  cvmsss2  32525  sdclem2  35021  dmmzp  39336  rnmpt0  41489  dvmptresicc  42210  dvcosax  42217  dvnprodlem3  42239  itgcoscmulx  42260  stoweidlem27  42319  dirkeritg  42394  fourierdlem16  42415  fourierdlem21  42420  fourierdlem22  42421  fourierdlem39  42438  fourierdlem57  42455  fourierdlem58  42456  fourierdlem60  42458  fourierdlem61  42459  fourierdlem73  42471  fourierdlem83  42481  subsaliuncllem  42647  0ome  42818  hoi2toco  42896  elbigofrcl  44617
  Copyright terms: Public domain W3C validator