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

Theorem ssralv 3546
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 3480 . . 3  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 75 . 2  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  ph )  ->  (
x  e.  A  ->  ph ) ) )
32ralimdv2 2848 1  |-  ( A 
C_  B  ->  ( A. x  e.  B  ph 
->  A. x  e.  A  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   A.wral 2791    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-ral 2796  df-in 3465  df-ss 3472
This theorem is referenced by:  intss  4289  iinss1  4324  disjiun  4423  poss  4788  sess2  4834  isores3  6212  isoini2  6216  smores  7021  smores2  7023  tfrlem5  7047  resixp  7502  ac6sfi  7762  iunfi  7806  ixpfi2  7816  dffi3  7889  marypha1lem  7891  ordtypelem2  7942  tcrank  8300  acndom  8430  pwsdompw  8582  ssfin3ds  8708  fin1a2s  8792  hsmexlem4  8807  domtriomlem  8820  zornn0g  8883  fpwwe2lem13  9018  ingru  9191  cshw1  12764  rexanuz  13152  cau3lem  13161  caubnd  13165  limsupgord  13269  limsupval2  13277  rlimres  13355  lo1res  13356  o1of2  13409  o1rlimmul  13415  isercolllem1  13461  climsup  13466  fsumiun  13609  pcfac  14290  vdwnnlem2  14386  firest  14702  imasaddfnlem  14797  imasvscafn  14806  psss  15713  tsrss  15722  cntz2ss  16239  cntzmhm2  16246  subgpgp  16486  efgsres  16625  telgsumfzs  16887  telgsums  16891  dprdss  16944  ocv2ss  18571  mretopd  19459  tgcn  19619  tgcnp  19620  subbascn  19621  cnss2  19644  cncnp  19647  sslm  19666  t1ficld  19694  tgcmp  19767  1stcfb  19812  islly2  19851  dislly  19864  comppfsc  19899  ptbasfi  19948  ptcnplem  19988  tx1stc  20017  qtoptop2  20066  fbunfip  20236  flftg  20363  txflf  20373  fclsbas  20388  fclsss1  20389  fclsss2  20390  alexsubb  20412  tmdgsum2  20461  metrest  20893  rescncf  21267  cnllycmp  21322  bndth  21324  fgcfil  21576  cfilres  21601  ivthlem2  21730  ivthlem3  21731  ovolsslem  21761  ovolfiniun  21778  finiunmbl  21820  volfiniun  21823  iunmbl  21829  ioombl1lem4  21837  dyadmax  21873  vitali  21888  mbfimaopnlem  21928  mbflimsup  21939  mbfi1flim  21996  ditgeq3  22120  dvferm  22255  rollelem  22256  dvivthlem1  22275  itgsubstlem  22315  aalioulem2  22594  ulmcaulem  22654  ulmss  22657  xrlimcnp  23163  lgsdchr  23488  pntlem3  23659  pntlemp  23660  pntleml  23661  nbgraf1olem1  24306  redwlk  24473  usg2wlkeq  24573  wwlknred  24588  wwlkm1edg  24600  clwlkisclwwlklem1  24652  clwwlkf  24659  wwlksubclwwlk  24669  extwwlkfablem2  24943  occon  26070  xrge0infss  27445  resspos  27513  resstos  27514  submarchi  27596  sigaclci  27998  measiun  28055  elmbfmvol2  28104  sibfof  28148  subfacp1lem3  28492  iccllyscon  28561  untint  28950  untangtr  28952  dfon2lem6  29188  dfon2lem8  29190  dfon2lem9  29191  setlikess  29243  poseq  29301  soseq  29302  finixpnum  30006  heicant  30017  volsupnfl  30027  neibastop1  30145  neibastop2lem  30146  neibastop3  30148  prdstotbnd  30258  heibor1lem  30273  ispridl2  30403  elrfirn2  30596  rabdiophlem1  30702  dford3lem1  30936  kelac1  30977  acsfn1p  31117  climinf  31516  ssralv2  33009  ssralv2VD  33374  bnj1118  33747
  Copyright terms: Public domain W3C validator