Theorem ssralv 3666

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

Step	Hyp	Ref	Expression
1		ssel 3597	. . 3 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	imim1d 82	. 2 |- ( A C_ B -> ( ( x e. B -> ph ) -> ( x e. A -> ph ) ) )
3	2	ralimdv2 2961	1 |- ( A C_ B -> ( A. x e. B ph -> A. x e. A ph ) )

Syntax hints:   -> wi 4   e. wcel 1990   A.wral 2912   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-in 3581  df-ss 3588

This theorem is referenced by:  intss  4498  iinss1  4533  disjiun  4640  poss  5037  sess2  5083  isores3  6585  isoini2  6589  smores  7449  smores2  7451  tfrlem5  7476  resixp  7943  ac6sfi  8204  iunfi  8254  ixpfi2  8264  dffi3  8337  marypha1lem  8339  ordtypelem2  8424  tcrank  8747  acndom  8874  pwsdompw  9026  ssfin3ds  9152  fin1a2s  9236  hsmexlem4  9251  domtriomlem  9264  zornn0g  9327  fpwwe2lem13  9464  ingru  9637  cshw1  13568  rexanuz  14085  cau3lem  14094  caubnd  14098  limsupgord  14203  limsupval2  14211  rlimres  14289  lo1res  14290  o1of2  14343  o1rlimmul  14349  isercolllem1  14395  climsup  14400  fsumiun  14553  lcmfunsnlem1  15350  coprmprod  15375  pcfac  15603  vdwnnlem2  15700  firest  16093  imasaddfnlem  16188  imasvscafn  16197  psss  17214  tsrss  17223  cntz2ss  17765  cntzmhm2  17772  subgpgp  18012  efgsres  18151  telgsumfzs  18386  telgsums  18390  dprdss  18428  ocv2ss  20017  mretopd  20896  tgcn  21056  tgcnp  21057  subbascn  21058  cnss2  21081  cncnp  21084  sslm  21103  t1ficld  21131  tgcmp  21204  1stcfb  21248  islly2  21287  dislly  21300  comppfsc  21335  ptbasfi  21384  ptcnplem  21424  tx1stc  21453  qtoptop2  21502  fbunfip  21673  flftg  21800  txflf  21810  fclsbas  21825  fclsss1  21826  fclsss2  21827  alexsubb  21850  tmdgsum2  21900  metrest  22329  rescncf  22700  cnllycmp  22755  bndth  22757  fgcfil  23069  cfilres  23094  ivthlem2  23221  ivthlem3  23222  ovolsslem  23252  ovolfiniun  23269  finiunmbl  23312  volfiniun  23315  iunmbl  23321  ioombl1lem4  23329  dyadmax  23366  vitali  23382  mbfimaopnlem  23422  mbflimsup  23433  mbfi1flim  23490  ditgeq3  23614  dvferm  23751  rollelem  23752  dvivthlem1  23771  itgsubstlem  23811  aalioulem2  24088  ulmcaulem  24148  ulmss  24151  xrlimcnp  24695  lgsdchr  25080  pntlem3  25298  pntlemp  25299  pntleml  25300  uspgr2wlkeq  26542  redwlk  26569  wwlksm1edg  26767  wwlksnred  26787  clwlkclwwlklem2  26901  clwwlkinwwlk  26905  clwwlksf  26915  wwlksubclwwlks  26925  occon  28146  xrge0infss  29525  resspos  29659  resstos  29660  submarchi  29740  sigaclci  30195  measiun  30281  elmbfmvol2  30329  sibfof  30402  ftc2re  30676  bnj1118  31052  subfacp1lem3  31164  iccllysconn  31232  untint  31589  untangtr  31591  dfon2lem6  31693  dfon2lem8  31695  dfon2lem9  31696  poseq  31750  soseq  31751  nosepon  31818  noresle  31846  sssslt1  31906  sssslt2  31907  neibastop1  32354  neibastop2lem  32355  neibastop3  32357  finixpnum  33394  ptrecube  33409  poimirlem26  33435  poimirlem27  33436  poimirlem30  33439  heicant  33444  volsupnfl  33454  prdstotbnd  33593  heibor1lem  33608  ispridl2  33837  elrfirn2  37259  rabdiophlem1  37365  dford3lem1  37593  kelac1  37633  acsfn1p  37769  ssralv2  38737  ssralv2VD  39102  climinf  39838  limsupvaluz2  39970  supcnvlimsup  39972  iccpartres  41354