Theorem ssralv 3983

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)

Assertion

Ref	Expression
ssralv	⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssralv

Step	Hyp	Ref	Expression
1		ssel 3910	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 82	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	ralimdv2 3101	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3063   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ss2ralv  3985  intss  4897  iinss1  4936  disjiun  5057  poss  5496  sess2  5549  isores3  7186  isoini2  7190  smores  8154  smores2  8156  tfrlem5  8182  resixp  8679  ac6sfi  8988  iunfi  9037  ixpfi2  9047  marypha1lem  9122  ordtypelem2  9208  tcrank  9573  acndom  9738  pwsdompw  9891  ssfin3ds  10017  fin1a2s  10101  hsmexlem4  10116  domtriomlem  10129  zornn0g  10192  fpwwe2lem12  10329  ingru  10502  cshw1  14463  rexanuz  14985  cau3lem  14994  caubnd  14998  limsupgord  15109  limsupval2  15117  rlimres  15195  lo1res  15196  o1of2  15250  o1rlimmul  15256  climsup  15309  fsumiun  15461  lcmfunsnlem1  16270  coprmprod  16294  pcfac  16528  vdwnnlem2  16625  firest  17060  imasaddfnlem  17156  imasvscafn  17165  psss  18213  tsrss  18222  cntz2ss  18854  cntzmhm2  18861  subgpgp  19117  efgsres  19259  telgsumfzs  19505  telgsums  19509  dprdss  19547  acsfn1p  19982  ocv2ss  20790  mretopd  22151  tgcn  22311  tgcnp  22312  subbascn  22313  cnss2  22336  cncnp  22339  sslm  22358  t1ficld  22386  tgcmp  22460  1stcfb  22504  islly2  22543  dislly  22556  comppfsc  22591  ptbasfi  22640  ptcnplem  22680  tx1stc  22709  qtoptop2  22758  fbunfip  22928  flftg  23055  txflf  23065  fclsbas  23080  fclsss1  23081  fclsss2  23082  alexsubb  23105  tmdgsum2  23155  metrest  23586  rescncf  23966  cnllycmp  24025  bndth  24027  fgcfil  24340  ivthlem2  24521  ivthlem3  24522  ovolsslem  24553  ovolfiniun  24570  finiunmbl  24613  volfiniun  24616  iunmbl  24622  ioombl1lem4  24630  dyadmax  24667  vitali  24682  mbfimaopnlem  24724  mbflimsup  24735  mbfi1flim  24793  ditgeq3  24919  dvferm  25057  rollelem  25058  dvivthlem1  25077  itgsubstlem  25117  aalioulem2  25398  ulmcaulem  25458  ulmss  25461  xrlimcnp  26023  2sqreunnlem2  26508  pntlem3  26662  pntlemp  26663  pntleml  26664  uspgr2wlkeq  27915  redwlk  27942  wwlksm1edg  28147  wwlksnred  28158  clwlkclwwlklem2  28265  clwwlkinwwlk  28305  clwwlkf  28312  wwlksubclwwlk  28323  occon  29550  xrge0infss  30985  resspos  31146  resstos  31147  gsummptres2  31215  submarchi  31342  prmidl2  31518  sigaclci  32000  measiun  32086  elmbfmvol2  32134  sibfof  32207  ftc2re  32478  bnj1118  32864  subfacp1lem3  33044  iccllysconn  33112  dmopab3rexdif  33267  untint  33553  untangtr  33555  dfon2lem6  33670  dfon2lem8  33672  dfon2lem9  33673  ttrclselem2  33712  xpord2ind  33721  xpord3ind  33727  poseq  33729  soseq  33730  naddssim  33764  nosepon  33795  noresle  33827  sssslt1  33916  sssslt2  33917  neibastop1  34475  neibastop2lem  34476  neibastop3  34478  finixpnum  35689  ptrecube  35704  poimirlem26  35730  poimirlem27  35731  poimirlem30  35734  heicant  35739  volsupnfl  35749  prdstotbnd  35879  heibor1lem  35894  ispridl2  36123  elrfirn2  40434  rabdiophlem1  40539  dford3lem1  40764  kelac1  40804  ssralv2  42040  ssralv2VD  42375  climinf  43037  limsupvaluz2  43169  supcnvlimsup  43171  iccpartres  44758