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

Theorem dmmptg 5509
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
Distinct variable group:   ,

Proof of Theorem dmmptg
StepHypRef Expression
1 elex 3118 . . . 4
21ralimi 2850 . . 3
3 rabid2 3035 . . 3
42, 3sylibr 212 . 2
5 eqid 2457 . . 3
65dmmpt 5507 . 2
74, 6syl6reqr 2517 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  A.wral 2807  {crab 2811   cvv 3109  e.cmpt 4510  domcdm 5004
This theorem is referenced by:  ovmpt3rabdm  6535  suppssov1  6951  suppssfv  6955  iinon  7030  onoviun  7033  noinfep  8097  cantnfdm  8102  cantnfdmOLD  8104  axcc2lem  8837  o1lo1  13360  o1lo12  13361  lo1mptrcl  13444  o1mptrcl  13445  o1add2  13446  o1mul2  13447  o1sub2  13448  lo1add  13449  lo1mul  13450  o1dif  13452  rlimneg  13469  lo1le  13474  rlimno1  13476  o1fsum  13627  divsfval  14944  iscnp2  19740  ptcnplem  20122  xkoinjcn  20188  fbasrn  20385  prdsdsf  20870  ressprdsds  20874  mbfmptcl  22044  mbfdm2  22045  dvmptcl  22362  dvmptadd  22363  dvmptmul  22364  dvmptres2  22365  dvmptcmul  22367  dvmptcj  22371  dvmptco  22375  rolle  22391  dvlip  22394  dvlipcn  22395  dvle  22408  dvivthlem1  22409  dvivth  22411  dvfsumle  22422  dvfsumge  22423  dvmptrecl  22425  dvfsumlem2  22428  pserdv  22824  logtayl  23041  rlimcxp  23303  o1cxp  23304  measdivcstOLD  28195  probfinmeasbOLD  28367  probmeasb  28369  dstrvprob  28410  cvmsss2  28719  sdclem2  30235  dmmzp  30665  dvmptresicc  31716  dvcosax  31723  dvnprodlem3  31745  itgcoscmulx  31768  stoweidlem27  31809  dirkeritg  31884  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem39  31928  fourierdlem57  31946  fourierdlem58  31947  fourierdlem60  31949  fourierdlem61  31950  fourierdlem73  31962  fourierdlem83  31972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-mpt 4512  df-xp 5010  df-rel 5011  df-cnv 5012  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017
  Copyright terms: Public domain W3C validator