Theorem ssralv 4012

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3911

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

This theorem depends on definitions:  df-bi 207  df-ral 3045  df-ss 3928

This theorem is referenced by:  ss2ralv  4014  intss  4929  iinss1  4967  disjiun  5090  poss  5541  sess2  5597  isores3  7292  isoini2  7296  xpord2indlem  8103  xpord3inddlem  8110  poseq  8114  soseq  8115  smores  8298  smores2  8300  tfrlem5  8325  naddssim  8626  resixp  8883  ac6sfi  9207  iunfi  9270  ixpfi2  9277  marypha1lem  9360  ordtypelem2  9448  ttrclselem2  9655  tcrank  9813  acndom  9980  pwsdompw  10132  ssfin3ds  10259  fin1a2s  10343  hsmexlem4  10358  domtriomlem  10371  zornn0g  10434  fpwwe2lem12  10571  ingru  10744  cshw1  14763  rexanuz  15288  cau3lem  15297  caubnd  15301  limsupgord  15414  limsupval2  15422  rlimres  15500  lo1res  15501  o1of2  15555  o1rlimmul  15561  climsup  15612  fsumiun  15763  lcmfunsnlem1  16583  coprmprod  16607  pcfac  16846  vdwnnlem2  16943  firest  17371  imasaddfnlem  17467  imasvscafn  17476  psss  18515  tsrss  18524  cntz2ss  19243  cntzmhm2  19250  subgpgp  19503  efgsres  19644  telgsumfzs  19895  telgsums  19899  dprdss  19937  acsfn1p  20684  ocv2ss  21558  mretopd  22955  tgcn  23115  tgcnp  23116  subbascn  23117  cnss2  23140  cncnp  23143  sslm  23162  t1ficld  23190  tgcmp  23264  1stcfb  23308  islly2  23347  dislly  23360  comppfsc  23395  ptbasfi  23444  ptcnplem  23484  tx1stc  23513  qtoptop2  23562  fbunfip  23732  flftg  23859  txflf  23869  fclsbas  23884  fclsss1  23885  fclsss2  23886  alexsubb  23909  tmdgsum2  23959  metrest  24388  rescncf  24766  cnllycmp  24831  bndth  24833  fgcfil  25147  ivthlem2  25329  ivthlem3  25330  ovolsslem  25361  ovolfiniun  25378  finiunmbl  25421  volfiniun  25424  iunmbl  25430  ioombl1lem4  25438  dyadmax  25475  vitali  25490  mbfimaopnlem  25532  mbflimsup  25543  mbfi1flim  25600  ditgeq3  25727  dvferm  25868  rollelem  25869  dvivthlem1  25889  itgsubstlem  25931  aalioulem2  26217  ulmcaulem  26279  ulmss  26282  xrlimcnp  26854  2sqreunnlem2  27342  pntlem3  27496  pntlemp  27497  pntleml  27498  nosepon  27553  noresle  27585  sssslt1  27683  sssslt2  27684  uspgr2wlkeq  29549  redwlk  29574  wwlksm1edg  29784  wwlksnred  29795  clwlkclwwlklem2  29902  clwwlkinwwlk  29942  clwwlkf  29949  wwlksubclwwlk  29960  occon  31189  xrge0infss  32656  resspos  32865  resstos  32866  gsummptres2  32966  submarchi  33113  prmidl2  33385  sigaclci  34095  measiun  34181  elmbfmvol2  34231  sibfof  34304  ftc2re  34562  bnj1118  34947  subfacp1lem3  35142  iccllysconn  35210  dmopab3rexdif  35365  untint  35672  untangtr  35674  dfon2lem6  35749  dfon2lem8  35751  dfon2lem9  35752  neibastop1  36320  neibastop2lem  36321  neibastop3  36323  weiunse  36429  finixpnum  37572  ptrecube  37587  poimirlem26  37613  poimirlem27  37614  poimirlem30  37617  heicant  37622  volsupnfl  37632  prdstotbnd  37761  heibor1lem  37776  ispridl2  38005  deg1gprod  42101  elrfirn2  42657  rabdiophlem1  42762  dford3lem1  42988  kelac1  43025  ssralv2  44494  ssralv2VD  44828  climinf  45577  limsupvaluz2  45709  supcnvlimsup  45711  iccpartres  47392  uhgrimisgrgric  47904  termc  49481