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

Theorem ssralv 3399
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 3334 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 71 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2778 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 1725   A.wral 2697    C_ wss 3312
This theorem is referenced by:  iinss1  4097  disjiun  4194  poss  4497  sess2  4543  isores3  6047  isoini2  6051  smores  6606  smores2  6608  tfrlem1  6628  resixp  7089  ac6sfi  7343  iunfi  7386  ixpfi2  7397  dffi3  7428  marypha1lem  7430  ordtypelem2  7480  tcrank  7800  acndom  7924  pwsdompw  8076  ssfin3ds  8202  fin1a2s  8286  hsmexlem4  8301  domtriomlem  8314  zornn0g  8377  fpwwe2lem13  8509  ingru  8682  rexanuz  12141  cau3lem  12150  caubnd  12154  limsupgord  12258  limsupval2  12266  rlimres  12344  lo1res  12345  o1of2  12398  o1rlimmul  12404  isercolllem1  12450  climsup  12455  fsumiun  12592  pcfac  13260  vdwnnlem2  13356  firest  13652  imasaddfnlem  13745  imasvscafn  13754  psss  14638  tsrss  14647  cntz2ss  15123  cntzmhm2  15130  subgpgp  15223  efgsres  15362  dprdss  15579  ocv2ss  16892  mretopd  17148  tgcn  17308  tgcnp  17309  subbascn  17310  cnss2  17333  cncnp  17336  sslm  17355  t1ficld  17383  tgcmp  17456  1stcfb  17500  islly2  17539  dislly  17552  ptbasfi  17605  ptcnplem  17645  tx1stc  17674  qtoptop2  17723  fbunfip  17893  flftg  18020  txflf  18030  fclsbas  18045  fclsss1  18046  fclsss2  18047  alexsubb  18069  tmdgsum2  18118  metrest  18546  rescncf  18919  cnllycmp  18973  bndth  18975  fgcfil  19216  cfilres  19241  ivthlem2  19341  ivthlem3  19342  ovolsslem  19372  ovolfiniun  19389  finiunmbl  19430  volfiniun  19433  iunmbl  19439  ioombl1lem4  19447  dyadmax  19482  vitali  19497  mbfimaopnlem  19539  mbflimsup  19550  mbfi1flim  19607  ditgeq3  19729  dvferm  19864  rollelem  19865  dvivthlem1  19884  itgsubstlem  19924  aalioulem2  20242  ulmcaulem  20302  ulmss  20305  xrlimcnp  20799  lgsdchr  21124  pntlem3  21295  pntlemp  21296  pntleml  21297  nbgraf1olem1  21443  redwlk  21598  occon  22781  resspos  24179  resstos  24180  sigaclci  24507  measiun  24564  elmbfmvol2  24609  sibfof  24646  subfacp1lem3  24860  iccllyscon  24929  untint  25153  untangtr  25155  dfon2lem6  25407  dfon2lem8  25409  dfon2lem9  25410  setlikess  25462  poseq  25520  soseq  25521  volsupnfl  26241  comppfsc  26378  neibastop1  26379  neibastop2lem  26380  neibastop3  26382  prdstotbnd  26494  heibor1lem  26509  ispridl2  26639  elrfirn2  26741  rabdiophlem1  26852  dford3lem1  27088  kelac1  27129  acsfn1p  27475  climinf  27699  cshw1  28238  ssralv2  28552  ssralv2VD  28915  bnj1118  29290
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-ral 2702  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator