Theorem ssralv 3999

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  ∀wral 3048   ⊆ wss 3898

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 3049  df-ss 3915

This theorem is referenced by:  ss2ralv  4001  intss  4921  iinss1  4959  disjiun  5083  poss  5531  sess2  5587  isores3  7278  isoini2  7282  xpord2indlem  8086  xpord3inddlem  8093  poseq  8097  soseq  8098  smores  8281  smores2  8283  tfrlem5  8308  naddssim  8609  resixp  8867  ac6sfi  9179  iunfi  9238  ixpfi2  9245  marypha1lem  9328  ordtypelem2  9416  ttrclselem2  9627  tcrank  9788  acndom  9953  pwsdompw  10105  ssfin3ds  10232  fin1a2s  10316  hsmexlem4  10331  domtriomlem  10344  zornn0g  10407  fpwwe2lem12  10544  ingru  10717  cshw1  14736  rexanuz  15260  cau3lem  15269  caubnd  15273  limsupgord  15386  limsupval2  15394  rlimres  15472  lo1res  15473  o1of2  15527  o1rlimmul  15533  climsup  15584  fsumiun  15735  lcmfunsnlem1  16555  coprmprod  16579  pcfac  16818  vdwnnlem2  16915  firest  17343  imasaddfnlem  17440  imasvscafn  17449  resspos  18343  resstos  18344  psss  18494  tsrss  18503  cntz2ss  19255  cntzmhm2  19262  subgpgp  19517  efgsres  19658  telgsumfzs  19909  telgsums  19913  dprdss  19951  acsfn1p  20723  ocv2ss  21619  mretopd  23027  tgcn  23187  tgcnp  23188  subbascn  23189  cnss2  23212  cncnp  23215  sslm  23234  t1ficld  23262  tgcmp  23336  1stcfb  23380  islly2  23419  dislly  23432  comppfsc  23467  ptbasfi  23516  ptcnplem  23556  tx1stc  23585  qtoptop2  23634  fbunfip  23804  flftg  23931  txflf  23941  fclsbas  23956  fclsss1  23957  fclsss2  23958  alexsubb  23981  tmdgsum2  24031  metrest  24459  rescncf  24837  cnllycmp  24902  bndth  24904  fgcfil  25218  ivthlem2  25400  ivthlem3  25401  ovolsslem  25432  ovolfiniun  25449  finiunmbl  25492  volfiniun  25495  iunmbl  25501  ioombl1lem4  25509  dyadmax  25546  vitali  25561  mbfimaopnlem  25603  mbflimsup  25614  mbfi1flim  25671  ditgeq3  25798  dvferm  25939  rollelem  25940  dvivthlem1  25960  itgsubstlem  26002  aalioulem2  26288  ulmcaulem  26350  ulmss  26353  xrlimcnp  26925  2sqreunnlem2  27413  pntlem3  27567  pntlemp  27568  pntleml  27569  nosepon  27624  noresle  27656  sssslt1  27756  sssslt2  27757  uspgr2wlkeq  29645  redwlk  29670  wwlksm1edg  29880  wwlksnred  29891  clwlkclwwlklem2  30001  clwwlkinwwlk  30041  clwwlkf  30048  wwlksubclwwlk  30059  occon  31288  xrge0infss  32768  gsummptres2  33064  submarchi  33196  prmidl2  33450  sigaclci  34217  measiun  34303  elmbfmvol2  34352  sibfof  34425  ftc2re  34683  bnj1118  35068  subfacp1lem3  35298  iccllysconn  35366  dmopab3rexdif  35521  untint  35828  untangtr  35830  dfon2lem6  35902  dfon2lem8  35904  dfon2lem9  35905  neibastop1  36475  neibastop2lem  36476  neibastop3  36478  weiunse  36584  finixpnum  37718  ptrecube  37733  poimirlem26  37759  poimirlem27  37760  poimirlem30  37763  heicant  37768  volsupnfl  37778  prdstotbnd  37907  heibor1lem  37922  ispridl2  38151  deg1gprod  42306  elrfirn2  42853  rabdiophlem1  42958  dford3lem1  43183  kelac1  43220  ssralv2  44688  ssralv2VD  45022  climinf  45768  limsupvaluz2  45898  supcnvlimsup  45900  iccpartres  47580  uhgrimisgrgric  48093  termc  49680