Theorem ssralv 3863

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 3792	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 82	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	ralimdv2 3149	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2156  ∀wral 3096   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-ral 3101  df-in 3776  df-ss 3783

This theorem is referenced by:  intss  4690  iinss1  4725  disjiun  4832  poss  5234  sess2  5280  isores3  6809  isoini2  6813  smores  7685  smores2  7687  tfrlem5  7712  resixp  8180  ac6sfi  8443  iunfi  8493  ixpfi2  8503  dffi3  8576  marypha1lem  8578  ordtypelem2  8663  tcrank  8994  acndom  9157  pwsdompw  9311  ssfin3ds  9437  fin1a2s  9521  hsmexlem4  9536  domtriomlem  9549  zornn0g  9612  fpwwe2lem13  9749  ingru  9922  cshw1  13792  rexanuz  14308  cau3lem  14317  caubnd  14321  limsupgord  14426  limsupval2  14434  rlimres  14512  lo1res  14513  o1of2  14566  o1rlimmul  14572  isercolllem1  14618  climsup  14623  fsumiun  14775  lcmfunsnlem1  15569  coprmprod  15593  pcfac  15820  vdwnnlem2  15917  firest  16298  imasaddfnlem  16393  imasvscafn  16402  psss  17419  tsrss  17428  cntz2ss  17966  cntzmhm2  17973  subgpgp  18213  efgsres  18352  telgsumfzs  18588  telgsums  18592  dprdss  18630  ocv2ss  20227  mretopd  21110  tgcn  21270  tgcnp  21271  subbascn  21272  cnss2  21295  cncnp  21298  sslm  21317  t1ficld  21345  tgcmp  21418  1stcfb  21462  islly2  21501  dislly  21514  comppfsc  21549  ptbasfi  21598  ptcnplem  21638  tx1stc  21667  qtoptop2  21716  fbunfip  21886  flftg  22013  txflf  22023  fclsbas  22038  fclsss1  22039  fclsss2  22040  alexsubb  22063  tmdgsum2  22113  metrest  22542  rescncf  22913  cnllycmp  22968  bndth  22970  fgcfil  23281  cfilres  23306  ivthlem2  23433  ivthlem3  23434  ovolsslem  23465  ovolfiniun  23482  finiunmbl  23525  volfiniun  23528  iunmbl  23534  ioombl1lem4  23542  dyadmax  23579  vitali  23594  mbfimaopnlem  23636  mbflimsup  23647  mbfi1flim  23704  ditgeq3  23828  dvferm  23965  rollelem  23966  dvivthlem1  23985  itgsubstlem  24025  aalioulem2  24302  ulmcaulem  24362  ulmss  24365  xrlimcnp  24909  lgsdchr  25294  pntlem3  25512  pntlemp  25513  pntleml  25514  uspgr2wlkeq  26770  redwlk  26797  wwlksm1edg  27008  wwlksnred  27029  clwlkclwwlklem2  27143  clwwlkinwwlk  27189  clwwlkf  27196  wwlksubclwwlk  27209  occon  28474  xrge0infss  29852  resspos  29984  resstos  29985  submarchi  30065  sigaclci  30520  measiun  30606  elmbfmvol2  30654  sibfof  30727  ftc2re  31001  bnj1118  31375  subfacp1lem3  31487  iccllysconn  31555  untint  31911  untangtr  31913  dfon2lem6  32013  dfon2lem8  32015  dfon2lem9  32016  poseq  32074  soseq  32075  nosepon  32139  noresle  32167  sssslt1  32227  sssslt2  32228  neibastop1  32675  neibastop2lem  32676  neibastop3  32678  finixpnum  33707  ptrecube  33722  poimirlem26  33748  poimirlem27  33749  poimirlem30  33752  heicant  33757  volsupnfl  33767  prdstotbnd  33904  heibor1lem  33919  ispridl2  34148  elrfirn2  37761  rabdiophlem1  37867  dford3lem1  38094  kelac1  38134  acsfn1p  38270  ssralv2  39235  ssralv2VD  39596  climinf  40318  limsupvaluz2  40450  supcnvlimsup  40452  iccpartres  41929