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

Theorem dmmptg 5620
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 3207 . . . 4 (𝐵𝑉𝐵 ∈ V)
21ralimi 2949 . . 3 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
3 rabid2 3113 . . 3 (𝐴 = {𝑥𝐴𝐵 ∈ V} ↔ ∀𝑥𝐴 𝐵 ∈ V)
42, 3sylibr 224 . 2 (∀𝑥𝐴 𝐵𝑉𝐴 = {𝑥𝐴𝐵 ∈ V})
5 eqid 2620 . . 3 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
65dmmpt 5618 . 2 dom (𝑥𝐴𝐵) = {𝑥𝐴𝐵 ∈ V}
74, 6syl6reqr 2673 1 (∀𝑥𝐴 𝐵𝑉 → dom (𝑥𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  wral 2909  {crab 2913  Vcvv 3195  cmpt 4720  dom cdm 5104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-mpt 4721  df-xp 5110  df-rel 5111  df-cnv 5112  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117
This theorem is referenced by:  ovmpt3rabdm  6877  suppssov1  7312  suppssfv  7316  iinon  7422  onoviun  7425  noinfep  8542  cantnfdm  8546  axcc2lem  9243  negfi  10956  ccatalpha  13358  swrd0  13416  o1lo1  14249  o1lo12  14250  lo1mptrcl  14333  o1mptrcl  14334  o1add2  14335  o1mul2  14336  o1sub2  14337  lo1add  14338  lo1mul  14339  o1dif  14341  rlimneg  14358  lo1le  14363  rlimno1  14365  o1fsum  14526  divsfval  16188  iscnp2  21024  ptcnplem  21405  xkoinjcn  21471  fbasrn  21669  prdsdsf  22153  ressprdsds  22157  mbfmptcl  23385  mbfdm2  23386  dvmptcl  23703  dvmptadd  23704  dvmptmul  23705  dvmptres2  23706  dvmptcmul  23708  dvmptcj  23712  dvmptco  23716  rolle  23734  dvlip  23737  dvlipcn  23738  dvle  23751  dvivthlem1  23752  dvivth  23754  dvfsumle  23765  dvfsumge  23766  dvmptrecl  23768  dvfsumlem2  23771  pserdv  24164  logtayl  24387  relogbf  24510  rlimcxp  24681  o1cxp  24682  gsummpt2co  29754  psgnfzto1stlem  29824  measdivcstOLD  30261  probfinmeasbOLD  30464  probmeasb  30466  dstrvprob  30507  cvmsss2  31230  sdclem2  33509  dmmzp  37115  rnmpt0  39228  dvmptresicc  39897  dvcosax  39904  dvnprodlem3  39926  itgcoscmulx  39948  stoweidlem27  40007  dirkeritg  40082  fourierdlem16  40103  fourierdlem21  40108  fourierdlem22  40109  fourierdlem39  40126  fourierdlem57  40143  fourierdlem58  40144  fourierdlem60  40146  fourierdlem61  40147  fourierdlem73  40159  fourierdlem83  40169  subsaliuncllem  40338  0ome  40506  hoi2toco  40584  elbigofrcl  42109
  Copyright terms: Public domain W3C validator