Theorem ssralv 4003

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 3919	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		imim1 83	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1834	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)))
4		df-ral 3076	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
5		df-ral 3076	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6	3, 4, 5	3imtr4g 298	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
7	1, 6	sylbi 219	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4  ∀wal 1557   ∈ wcel 2141  ∀wral 3075   ⊆ wss 3902

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

This theorem depends on definitions:  df-bi 209  df-ral 3076  df-ss 3919

This theorem is referenced by:  ss2ralv  4005  intss  4924  iinss1  4962  disjiun  5085  poss  5553  sess2  5609  isores3  7314  isoini2  7318  xpord2indlem  8121  xpord3inddlem  8128  poseq  8132  soseq  8133  smores  8317  smores2  8319  tfrlem5  8344  naddssim  8650  resixp  8909  ac6sfi  9222  iunfi  9280  ixpfi2  9287  marypha1lem  9373  ordtypelem2  9461  ttrclselem2  9675  tcrank  9836  acndom  10001  pwsdompw  10153  ssfin3ds  10281  fin1a2s  10365  hsmexlem4  10380  domtriomlem  10393  zornn0g  10456  fpwwe2lem12  10594  ingru  10767  cshw1  14829  rexanuz  15364  cau3lem  15373  caubnd  15377  limsupgord  15490  limsupval2  15498  rlimres  15576  lo1res  15577  o1of2  15631  o1rlimmul  15637  climsup  15688  fsumiun  15840  lcmfunsnlem1  16662  coprmprod  16686  pcfac  16926  vdwnnlem2  17023  firest  17452  imasaddfnlem  17549  imasvscafn  17558  resspos  18452  resstos  18453  psss  18603  tsrss  18612  cntz2ss  19366  cntzmhm2  19373  subgpgp  19628  efgsres  19769  telgsumfzs  20020  telgsums  20024  dprdss  20062  acsfn1p  20836  ocv2ss  21713  mretopd  23140  tgcn  23300  tgcnp  23301  subbascn  23302  cnss2  23325  cncnp  23328  sslm  23347  t1ficld  23375  tgcmp  23449  1stcfb  23493  islly2  23532  dislly  23545  comppfsc  23580  ptbasfi  23629  ptcnplem  23669  tx1stc  23698  qtoptop2  23747  fbunfip  23917  flftg  24044  txflf  24054  fclsbas  24069  fclsss1  24070  fclsss2  24071  alexsubb  24094  tmdgsum2  24144  metrest  24572  rescncf  24947  cnllycmp  25006  bndth  25008  fgcfil  25321  ivthlem2  25502  ivthlem3  25503  ovolsslem  25534  ovolfiniun  25551  finiunmbl  25594  volfiniun  25597  iunmbl  25603  ioombl1lem4  25611  dyadmax  25648  vitali  25663  mbfimaopnlem  25705  mbflimsup  25716  mbfi1flim  25773  ditgeq3  25900  dvferm  26038  rollelem  26039  dvivthlem1  26058  itgsubstlem  26098  aalioulem2  26385  ulmcaulem  26445  ulmss  26448  xrlimcnp  27021  2sqreunnlem2  27507  pntlem3  27661  pntlemp  27662  pntleml  27663  nosepon  27717  noresle  27749  ssslts1  27854  ssslts2  27855  uspgr2wlkeq  29803  redwlk  29828  wwlksm1edg  30038  wwlksnred  30049  clwlkclwwlklem2  30159  clwwlkinwwlk  30199  clwwlkf  30206  wwlksubclwwlk  30217  occon  31447  xrge0infss  32923  gsummptres2  33194  submarchi  33327  prmidl2  33588  sigaclci  34390  measiun  34476  elmbfmvol2  34525  sibfof  34598  ftc2re  34853  bnj1118  35240  subfacp1lem3  35493  iccllysconn  35561  dmopab3rexdif  35716  untint  36023  untangtr  36025  dfon2lem6  36097  dfon2lem8  36099  dfon2lem9  36100  neibastop1  36680  neibastop2lem  36681  neibastop3  36683  weiunse  36789  finixpnum  38065  ptrecube  38080  poimirlem26  38106  poimirlem27  38107  poimirlem30  38110  heicant  38115  volsupnfl  38125  prdstotbnd  38254  heibor1lem  38269  ispridl2  38498  deg1gprod  42718  elrfirn2  43238  rabdiophlem1  43339  dford3lem1  43564  kelac1  43601  ssralv2  45068  ssralv2VD  45402  climinf  46143  limsupvaluz2  46273  supcnvlimsup  46275  iccpartres  47985  uhgrimisgrgric  48514  termc  50101