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 84	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1845	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)))
4		df-ral 3080	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
5		df-ral 3080	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
7	1, 6	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4  ∀wal 1568   ∈ wcel 2143  ∀wral 3079   ⊆ wss 3905

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

This theorem depends on definitions:  df-bi 210  df-ral 3080  df-ss 3922

This theorem is referenced by:  ss2ralv  4008  intss  4934  iinss1  4972  disjiun  5097  poss  5571  sess2  5627  isores3  7333  isoini2  7337  xpord2indlem  8139  xpord3inddlem  8146  poseq  8150  soseq  8151  smores  8335  smores2  8337  tfrlem5  8362  naddssim  8668  resixp  8927  ac6sfi  9240  iunfi  9296  ixpfi2  9303  marypha1lem  9389  ordtypelem2  9477  ttrclselem2  9691  tcrank  9852  acndom  10031  pwsdompw  10182  ssfin3ds  10309  fin1a2s  10393  hsmexlem4  10408  domtriomlem  10421  zornn0g  10484  fpwwe2lem12  10622  ingru  10795  cshw1  14855  rexanuz  15393  cau3lem  15402  caubnd  15406  limsupgord  15519  limsupval2  15527  rlimres  15605  lo1res  15606  o1of2  15660  o1rlimmul  15666  climsup  15717  fsumiun  15869  lcmfunsnlem1  16690  coprmprod  16714  pcfac  16954  vdwnnlem2  17051  firest  17480  imasaddfnlem  17577  imasvscafn  17586  resspos  18480  resstos  18481  psss  18631  tsrss  18640  cntz2ss  19400  cntzmhm2  19407  subgpgp  19662  efgsres  19803  telgsumfzs  20054  telgsums  20058  dprdss  20096  acsfn1p  20902  prmidl2  21466  ocv2ss  21823  mretopd  23249  tgcn  23409  tgcnp  23410  subbascn  23411  cnss2  23434  cncnp  23437  sslm  23456  t1ficld  23484  tgcmp  23558  1stcfb  23602  islly2  23641  dislly  23654  comppfsc  23689  ptbasfi  23738  ptcnplem  23778  tx1stc  23807  qtoptop2  23856  fbunfip  24026  flftg  24153  txflf  24163  fclsbas  24178  fclsss1  24179  fclsss2  24180  alexsubb  24203  tmdgsum2  24253  metrest  24681  rescncf  25056  cnllycmp  25115  bndth  25117  fgcfil  25430  ivthlem2  25611  ivthlem3  25612  ovolsslem  25643  ovolfiniun  25660  finiunmbl  25703  volfiniun  25706  iunmbl  25712  ioombl1lem4  25720  dyadmax  25757  vitali  25772  mbfimaopnlem  25814  mbflimsup  25825  mbfi1flim  25882  ditgeq3  26009  dvferm  26147  rollelem  26148  dvivthlem1  26167  itgsubstlem  26207  aalioulem2  26496  ulmcaulem  26557  ulmss  26560  xrlimcnp  27133  2sqreunnlem2  27619  pntlem3  27773  pntlemp  27774  pntleml  27775  nosepon  27829  noresle  27861  ssslts1  27966  ssslts2  27967  uspgr2wlkeq  29995  redwlk  30020  wwlksm1edg  30230  wwlksnred  30241  clwlkclwwlklem2  30351  clwwlkinwwlk  30391  clwwlkf  30398  wwlksubclwwlk  30409  occon  31639  xrge0infss  33105  gsummptres2  33373  submarchi  33506  sigaclci  34522  measiun  34608  elmbfmvol2  34657  sibfof  34730  ftc2re  34985  bnj1118  35372  subfacp1lem3  35674  iccllysconn  35742  dmopab3rexdif  35897  untint  36204  untangtr  36206  dfon2lem6  36278  dfon2lem8  36280  dfon2lem9  36281  neibastop1  36870  neibastop2lem  36871  neibastop3  36873  weiunse  36979  finixpnum  38256  ptrecube  38271  poimirlem26  38297  poimirlem27  38298  poimirlem30  38301  heicant  38306  volsupnfl  38316  prdstotbnd  38445  heibor1lem  38460  ispridl2  38689  deg1gprod  42907  elrfirn2  43427  rabdiophlem1  43528  dford3lem1  43753  kelac1  43790  ssralv2  45240  ssralv2VD  45574  climinf  46322  limsupvaluz2  46452  supcnvlimsup  46454  iccpartres  48167  uhgrimisgrgric  48696  termc  50297