Theorem ssralv 4006

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 3922	. 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 3905

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 3922

This theorem is referenced by:  ss2ralv  4008  intss  4922  iinss1  4960  disjiun  5083  poss  5533  sess2  5589  isores3  7276  isoini2  7280  xpord2indlem  8087  xpord3inddlem  8094  poseq  8098  soseq  8099  smores  8282  smores2  8284  tfrlem5  8309  naddssim  8610  resixp  8867  ac6sfi  9189  iunfi  9252  ixpfi2  9259  marypha1lem  9342  ordtypelem2  9430  ttrclselem2  9641  tcrank  9799  acndom  9964  pwsdompw  10116  ssfin3ds  10243  fin1a2s  10327  hsmexlem4  10342  domtriomlem  10355  zornn0g  10418  fpwwe2lem12  10555  ingru  10728  cshw1  14747  rexanuz  15272  cau3lem  15281  caubnd  15285  limsupgord  15398  limsupval2  15406  rlimres  15484  lo1res  15485  o1of2  15539  o1rlimmul  15545  climsup  15596  fsumiun  15747  lcmfunsnlem1  16567  coprmprod  16591  pcfac  16830  vdwnnlem2  16927  firest  17355  imasaddfnlem  17451  imasvscafn  17460  resspos  18354  resstos  18355  psss  18505  tsrss  18514  cntz2ss  19233  cntzmhm2  19240  subgpgp  19495  efgsres  19636  telgsumfzs  19887  telgsums  19891  dprdss  19929  acsfn1p  20703  ocv2ss  21599  mretopd  22996  tgcn  23156  tgcnp  23157  subbascn  23158  cnss2  23181  cncnp  23184  sslm  23203  t1ficld  23231  tgcmp  23305  1stcfb  23349  islly2  23388  dislly  23401  comppfsc  23436  ptbasfi  23485  ptcnplem  23525  tx1stc  23554  qtoptop2  23603  fbunfip  23773  flftg  23900  txflf  23910  fclsbas  23925  fclsss1  23926  fclsss2  23927  alexsubb  23950  tmdgsum2  24000  metrest  24429  rescncf  24807  cnllycmp  24872  bndth  24874  fgcfil  25188  ivthlem2  25370  ivthlem3  25371  ovolsslem  25402  ovolfiniun  25419  finiunmbl  25462  volfiniun  25465  iunmbl  25471  ioombl1lem4  25479  dyadmax  25516  vitali  25531  mbfimaopnlem  25573  mbflimsup  25584  mbfi1flim  25641  ditgeq3  25768  dvferm  25909  rollelem  25910  dvivthlem1  25930  itgsubstlem  25972  aalioulem2  26258  ulmcaulem  26320  ulmss  26323  xrlimcnp  26895  2sqreunnlem2  27383  pntlem3  27537  pntlemp  27538  pntleml  27539  nosepon  27594  noresle  27626  sssslt1  27725  sssslt2  27726  uspgr2wlkeq  29610  redwlk  29635  wwlksm1edg  29845  wwlksnred  29856  clwlkclwwlklem2  29963  clwwlkinwwlk  30003  clwwlkf  30010  wwlksubclwwlk  30021  occon  31250  xrge0infss  32722  gsummptres2  33025  submarchi  33147  prmidl2  33397  sigaclci  34118  measiun  34204  elmbfmvol2  34254  sibfof  34327  ftc2re  34585  bnj1118  34970  subfacp1lem3  35174  iccllysconn  35242  dmopab3rexdif  35397  untint  35704  untangtr  35706  dfon2lem6  35781  dfon2lem8  35783  dfon2lem9  35784  neibastop1  36352  neibastop2lem  36353  neibastop3  36355  weiunse  36461  finixpnum  37604  ptrecube  37619  poimirlem26  37645  poimirlem27  37646  poimirlem30  37649  heicant  37654  volsupnfl  37664  prdstotbnd  37793  heibor1lem  37808  ispridl2  38037  deg1gprod  42133  elrfirn2  42689  rabdiophlem1  42794  dford3lem1  43019  kelac1  43056  ssralv2  44525  ssralv2VD  44859  climinf  45607  limsupvaluz2  45739  supcnvlimsup  45741  iccpartres  47422  uhgrimisgrgric  47935  termc  49524