Theorem ssralv 3983

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.) Avoid axioms. (Revised by GG, 19-May-2025.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssralv

Step	Hyp	Ref	Expression
1		df-ss 3900	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		imim1 83	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1822	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)))
4		df-ral 3054	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
5		df-ral 3054	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6	3, 4, 5	3imtr4g 297	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
7	1, 6	sylbi 218	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119  ∀wral 3053   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816

This theorem depends on definitions:  df-bi 208  df-ral 3054  df-ss 3900

This theorem is referenced by:  ss2ralv  3985  intss  4899  iinss1  4937  disjiun  5060  poss  5528  sess2  5584  isores3  7279  isoini2  7283  xpord2indlem  8087  xpord3inddlem  8094  poseq  8098  soseq  8099  smores  8282  smores2  8284  tfrlem5  8309  naddssim  8611  resixp  8871  ac6sfi  9184  iunfi  9243  ixpfi2  9250  marypha1lem  9336  ordtypelem2  9424  ttrclselem2  9638  tcrank  9799  acndom  9964  pwsdompw  10116  ssfin3ds  10243  fin1a2s  10327  hsmexlem4  10342  domtriomlem  10355  zornn0g  10418  fpwwe2lem12  10556  ingru  10729  cshw1  14775  rexanuz  15299  cau3lem  15308  caubnd  15312  limsupgord  15425  limsupval2  15433  rlimres  15511  lo1res  15512  o1of2  15566  o1rlimmul  15572  climsup  15623  fsumiun  15775  lcmfunsnlem1  16597  coprmprod  16621  pcfac  16861  vdwnnlem2  16958  firest  17386  imasaddfnlem  17483  imasvscafn  17492  resspos  18386  resstos  18387  psss  18537  tsrss  18546  cntz2ss  19301  cntzmhm2  19308  subgpgp  19563  efgsres  19704  telgsumfzs  19955  telgsums  19959  dprdss  19997  acsfn1p  20771  ocv2ss  21648  mretopd  23075  tgcn  23235  tgcnp  23236  subbascn  23237  cnss2  23260  cncnp  23263  sslm  23282  t1ficld  23310  tgcmp  23384  1stcfb  23428  islly2  23467  dislly  23480  comppfsc  23515  ptbasfi  23564  ptcnplem  23604  tx1stc  23633  qtoptop2  23682  fbunfip  23852  flftg  23979  txflf  23989  fclsbas  24004  fclsss1  24005  fclsss2  24006  alexsubb  24029  tmdgsum2  24079  metrest  24507  rescncf  24882  cnllycmp  24941  bndth  24943  fgcfil  25256  ivthlem2  25437  ivthlem3  25438  ovolsslem  25469  ovolfiniun  25486  finiunmbl  25529  volfiniun  25532  iunmbl  25538  ioombl1lem4  25546  dyadmax  25583  vitali  25598  mbfimaopnlem  25640  mbflimsup  25651  mbfi1flim  25708  ditgeq3  25835  dvferm  25973  rollelem  25974  dvivthlem1  25993  itgsubstlem  26033  aalioulem2  26317  ulmcaulem  26377  ulmss  26380  xrlimcnp  26950  2sqreunnlem2  27436  pntlem3  27590  pntlemp  27591  pntleml  27592  nosepon  27647  noresle  27679  ssslts1  27783  ssslts2  27784  uspgr2wlkeq  29732  redwlk  29757  wwlksm1edg  29967  wwlksnred  29978  clwlkclwwlklem2  30088  clwwlkinwwlk  30128  clwwlkf  30135  wwlksubclwwlk  30146  occon  31376  xrge0infss  32852  gsummptres2  33134  submarchi  33267  prmidl2  33524  sigaclci  34316  measiun  34402  elmbfmvol2  34451  sibfof  34524  ftc2re  34782  bnj1118  35166  subfacp1lem3  35410  iccllysconn  35478  dmopab3rexdif  35633  untint  35940  untangtr  35942  dfon2lem6  36014  dfon2lem8  36016  dfon2lem9  36017  neibastop1  36587  neibastop2lem  36588  neibastop3  36590  weiunse  36696  finixpnum  37972  ptrecube  37987  poimirlem26  38013  poimirlem27  38014  poimirlem30  38017  heicant  38022  volsupnfl  38032  prdstotbnd  38161  heibor1lem  38176  ispridl2  38405  deg1gprod  42625  elrfirn2  43145  rabdiophlem1  43246  dford3lem1  43471  kelac1  43508  ssralv2  44975  ssralv2VD  45309  climinf  46051  limsupvaluz2  46181  supcnvlimsup  46183  iccpartres  47893  uhgrimisgrgric  48422  termc  50009