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

Theorem dmmptg 5670
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 3243 . . . 4 (𝐵𝑉𝐵 ∈ V)
21ralimi 2981 . . 3 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 𝐵 ∈ V)
3 rabid2 3148 . . 3 (𝐴 = {𝑥𝐴𝐵 ∈ V} ↔ ∀𝑥𝐴 𝐵 ∈ V)
42, 3sylibr 224 . 2 (∀𝑥𝐴 𝐵𝑉𝐴 = {𝑥𝐴𝐵 ∈ V})
5 eqid 2651 . . 3 (𝑥𝐴𝐵) = (𝑥𝐴𝐵)
65dmmpt 5668 . 2 dom (𝑥𝐴𝐵) = {𝑥𝐴𝐵 ∈ V}
74, 6syl6reqr 2704 1 (∀𝑥𝐴 𝐵𝑉 → dom (𝑥𝐴𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  wral 2941  {crab 2945  Vcvv 3231  cmpt 4762  dom cdm 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-mpt 4763  df-xp 5149  df-rel 5150  df-cnv 5151  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156
This theorem is referenced by:  ovmpt3rabdm  6934  suppssov1  7372  suppssfv  7376  iinon  7482  onoviun  7485  noinfep  8595  cantnfdm  8599  axcc2lem  9296  negfi  11009  ccatalpha  13411  swrd0  13480  o1lo1  14312  o1lo12  14313  lo1mptrcl  14396  o1mptrcl  14397  o1add2  14398  o1mul2  14399  o1sub2  14400  lo1add  14401  lo1mul  14402  o1dif  14404  rlimneg  14421  lo1le  14426  rlimno1  14428  o1fsum  14589  divsfval  16254  iscnp2  21091  ptcnplem  21472  xkoinjcn  21538  fbasrn  21735  prdsdsf  22219  ressprdsds  22223  mbfmptcl  23449  mbfdm2  23450  dvmptcl  23767  dvmptadd  23768  dvmptmul  23769  dvmptres2  23770  dvmptcmul  23772  dvmptcj  23776  dvmptco  23780  rolle  23798  dvlip  23801  dvlipcn  23802  dvle  23815  dvivthlem1  23816  dvivth  23818  dvfsumle  23829  dvfsumge  23830  dvmptrecl  23832  dvfsumlem2  23835  pserdv  24228  logtayl  24451  relogbf  24574  rlimcxp  24745  o1cxp  24746  gsummpt2co  29908  psgnfzto1stlem  29978  measdivcstOLD  30415  probfinmeasbOLD  30618  probmeasb  30620  dstrvprob  30661  cvmsss2  31382  sdclem2  33668  dmmzp  37613  rnmpt0  39726  dvmptresicc  40452  dvcosax  40459  dvnprodlem3  40481  itgcoscmulx  40503  stoweidlem27  40562  dirkeritg  40637  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem39  40681  fourierdlem57  40698  fourierdlem58  40699  fourierdlem60  40701  fourierdlem61  40702  fourierdlem73  40714  fourierdlem83  40724  subsaliuncllem  40893  0ome  41064  hoi2toco  41142  elbigofrcl  42669
  Copyright terms: Public domain W3C validator