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

Theorem ssralv 3237
Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)
Assertion
Ref Expression
ssralv  |-  ( A 
C_  B  ->  ( A. x  e.  B  ph 
->  A. x  e.  A  ph ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem ssralv
StepHypRef Expression
1 ssel 3174 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 69 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2623 1  |-  ( A 
C_  B  ->  ( A. x  e.  B  ph 
->  A. x  e.  A  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   A.wral 2543    C_ wss 3152
This theorem is referenced by:  iinss1  3917  disjiun  4013  poss  4316  sess2  4362  isores3  5832  isoini2  5836  smores  6369  smores2  6371  tfrlem1  6391  resixp  6851  ac6sfi  7101  iunfi  7144  ixpfi2  7154  dffi3  7184  marypha1lem  7186  ordtypelem2  7234  tcrank  7554  acndom  7678  pwsdompw  7830  ssfin3ds  7956  fin1a2s  8040  hsmexlem4  8055  domtriomlem  8068  zornn0g  8132  fpwwe2lem13  8264  ingru  8437  rexanuz  11829  cau3lem  11838  caubnd  11842  limsupgord  11946  limsupval2  11954  rlimres  12032  lo1res  12033  o1of2  12086  o1rlimmul  12092  isercolllem1  12138  climsup  12143  fsumiun  12279  pcfac  12947  vdwnnlem2  13043  firest  13337  imasaddfnlem  13430  imasvscafn  13439  psss  14323  tsrss  14332  cntz2ss  14808  cntzmhm2  14815  subgpgp  14908  efgsres  15047  dprdss  15264  ocv2ss  16573  mretopd  16829  tgcn  16982  tgcnp  16983  subbascn  16984  cnss2  17006  cncnp  17009  sslm  17027  t1ficld  17055  tgcmp  17128  1stcfb  17171  islly2  17210  dislly  17223  ptbasfi  17276  ptcnplem  17315  tx1stc  17344  qtoptop2  17390  fbunfip  17564  flftg  17691  txflf  17701  fclsbas  17716  fclsss1  17717  fclsss2  17718  alexsubb  17740  tmdgsum2  17779  metrest  18070  rescncf  18401  cnllycmp  18454  bndth  18456  fgcfil  18697  cfilres  18722  ivthlem2  18812  ivthlem3  18813  ovolsslem  18843  ovolfiniun  18860  finiunmbl  18901  volfiniun  18904  iunmbl  18910  ioombl1lem4  18918  dyadmax  18953  vitali  18968  mbfimaopnlem  19010  mbflimsup  19021  mbfi1flim  19078  ditgeq3  19200  dvferm  19335  rollelem  19336  dvivthlem1  19355  itgsubstlem  19395  aalioulem2  19713  ulmcaulem  19771  ulmss  19774  xrlimcnp  20263  lgsdchr  20587  pntlem3  20758  pntlemp  20759  pntleml  20760  occon  21866  subfacp1lem3  23124  iccllyscon  23192  untint  23469  untangtr  23471  dfon2lem6  23555  dfon2lem8  23557  dfon2lem9  23558  setlikess  23606  poseq  23664  soseq  23665  ubpar  24673  lvsovso3  25040  comppfsc  25719  neibastop1  25720  neibastop2lem  25721  neibastop3  25723  prdstotbnd  25930  heibor1lem  25945  ispridl2  26075  elrfirn2  26183  rabdiophlem1  26294  dford3lem1  26531  kelac1  26573  acsfn1p  26919  climinf  27144  ssralv2  27667  ssralv2VD  28015  bnj1118  28387
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator