Theorem ssralv 3998

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 3914	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		imim1 83	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1816	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)))
4		df-ral 3048	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
5		df-ral 3048	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
7	1, 6	sylbi 217	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  ∀wral 3047   ⊆ wss 3897

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

This theorem depends on definitions:  df-bi 207  df-ral 3048  df-ss 3914

This theorem is referenced by:  ss2ralv  4000  intss  4919  iinss1  4957  disjiun  5081  poss  5529  sess2  5585  isores3  7275  isoini2  7279  xpord2indlem  8083  xpord3inddlem  8090  poseq  8094  soseq  8095  smores  8278  smores2  8280  tfrlem5  8305  naddssim  8606  resixp  8863  ac6sfi  9174  iunfi  9233  ixpfi2  9240  marypha1lem  9323  ordtypelem2  9411  ttrclselem2  9622  tcrank  9783  acndom  9948  pwsdompw  10100  ssfin3ds  10227  fin1a2s  10311  hsmexlem4  10326  domtriomlem  10339  zornn0g  10402  fpwwe2lem12  10539  ingru  10712  cshw1  14735  rexanuz  15259  cau3lem  15268  caubnd  15272  limsupgord  15385  limsupval2  15393  rlimres  15471  lo1res  15472  o1of2  15526  o1rlimmul  15532  climsup  15583  fsumiun  15734  lcmfunsnlem1  16554  coprmprod  16578  pcfac  16817  vdwnnlem2  16914  firest  17342  imasaddfnlem  17438  imasvscafn  17447  resspos  18341  resstos  18342  psss  18492  tsrss  18501  cntz2ss  19253  cntzmhm2  19260  subgpgp  19515  efgsres  19656  telgsumfzs  19907  telgsums  19911  dprdss  19949  acsfn1p  20720  ocv2ss  21616  mretopd  23013  tgcn  23173  tgcnp  23174  subbascn  23175  cnss2  23198  cncnp  23201  sslm  23220  t1ficld  23248  tgcmp  23322  1stcfb  23366  islly2  23405  dislly  23418  comppfsc  23453  ptbasfi  23502  ptcnplem  23542  tx1stc  23571  qtoptop2  23620  fbunfip  23790  flftg  23917  txflf  23927  fclsbas  23942  fclsss1  23943  fclsss2  23944  alexsubb  23967  tmdgsum2  24017  metrest  24445  rescncf  24823  cnllycmp  24888  bndth  24890  fgcfil  25204  ivthlem2  25386  ivthlem3  25387  ovolsslem  25418  ovolfiniun  25435  finiunmbl  25478  volfiniun  25481  iunmbl  25487  ioombl1lem4  25495  dyadmax  25532  vitali  25547  mbfimaopnlem  25589  mbflimsup  25600  mbfi1flim  25657  ditgeq3  25784  dvferm  25925  rollelem  25926  dvivthlem1  25946  itgsubstlem  25988  aalioulem2  26274  ulmcaulem  26336  ulmss  26339  xrlimcnp  26911  2sqreunnlem2  27399  pntlem3  27553  pntlemp  27554  pntleml  27555  nosepon  27610  noresle  27642  sssslt1  27742  sssslt2  27743  uspgr2wlkeq  29631  redwlk  29656  wwlksm1edg  29866  wwlksnred  29877  clwlkclwwlklem2  29987  clwwlkinwwlk  30027  clwwlkf  30034  wwlksubclwwlk  30045  occon  31274  xrge0infss  32750  gsummptres2  33040  submarchi  33162  prmidl2  33413  sigaclci  34152  measiun  34238  elmbfmvol2  34287  sibfof  34360  ftc2re  34618  bnj1118  35003  subfacp1lem3  35233  iccllysconn  35301  dmopab3rexdif  35456  untint  35763  untangtr  35765  dfon2lem6  35837  dfon2lem8  35839  dfon2lem9  35840  neibastop1  36410  neibastop2lem  36411  neibastop3  36413  weiunse  36519  finixpnum  37651  ptrecube  37666  poimirlem26  37692  poimirlem27  37693  poimirlem30  37696  heicant  37701  volsupnfl  37711  prdstotbnd  37840  heibor1lem  37855  ispridl2  38084  deg1gprod  42239  elrfirn2  42794  rabdiophlem1  42899  dford3lem1  43124  kelac1  43161  ssralv2  44629  ssralv2VD  44963  climinf  45711  limsupvaluz2  45841  supcnvlimsup  45843  iccpartres  47523  uhgrimisgrgric  48036  termc  49625