Theorem ssralv 4063

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

Syntax hints:   → wi 4  ∀wal 1534   ∈ wcel 2105  ∀wral 3058   ⊆ wss 3962

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

This theorem depends on definitions:  df-bi 207  df-ral 3059  df-ss 3979

This theorem is referenced by:  ss2ralv  4065  intss  4973  iinss1  5011  disjiun  5135  poss  5598  sess2  5654  isores3  7354  isoini2  7358  xpord2indlem  8170  xpord3inddlem  8177  poseq  8181  soseq  8182  smores  8390  smores2  8392  tfrlem5  8418  naddssim  8721  resixp  8971  ac6sfi  9317  iunfi  9380  ixpfi2  9387  marypha1lem  9470  ordtypelem2  9556  ttrclselem2  9763  tcrank  9921  acndom  10088  pwsdompw  10240  ssfin3ds  10367  fin1a2s  10451  hsmexlem4  10466  domtriomlem  10479  zornn0g  10542  fpwwe2lem12  10679  ingru  10852  cshw1  14856  rexanuz  15380  cau3lem  15389  caubnd  15393  limsupgord  15504  limsupval2  15512  rlimres  15590  lo1res  15591  o1of2  15645  o1rlimmul  15651  climsup  15702  fsumiun  15853  lcmfunsnlem1  16670  coprmprod  16694  pcfac  16932  vdwnnlem2  17029  firest  17478  imasaddfnlem  17574  imasvscafn  17583  psss  18637  tsrss  18646  cntz2ss  19365  cntzmhm2  19372  subgpgp  19629  efgsres  19770  telgsumfzs  20021  telgsums  20025  dprdss  20063  acsfn1p  20816  ocv2ss  21708  mretopd  23115  tgcn  23275  tgcnp  23276  subbascn  23277  cnss2  23300  cncnp  23303  sslm  23322  t1ficld  23350  tgcmp  23424  1stcfb  23468  islly2  23507  dislly  23520  comppfsc  23555  ptbasfi  23604  ptcnplem  23644  tx1stc  23673  qtoptop2  23722  fbunfip  23892  flftg  24019  txflf  24029  fclsbas  24044  fclsss1  24045  fclsss2  24046  alexsubb  24069  tmdgsum2  24119  metrest  24552  rescncf  24936  cnllycmp  25001  bndth  25003  fgcfil  25318  ivthlem2  25500  ivthlem3  25501  ovolsslem  25532  ovolfiniun  25549  finiunmbl  25592  volfiniun  25595  iunmbl  25601  ioombl1lem4  25609  dyadmax  25646  vitali  25661  mbfimaopnlem  25703  mbflimsup  25714  mbfi1flim  25772  ditgeq3  25899  dvferm  26040  rollelem  26041  dvivthlem1  26061  itgsubstlem  26103  aalioulem2  26389  ulmcaulem  26451  ulmss  26454  xrlimcnp  27025  2sqreunnlem2  27513  pntlem3  27667  pntlemp  27668  pntleml  27669  nosepon  27724  noresle  27756  sssslt1  27854  sssslt2  27855  uspgr2wlkeq  29678  redwlk  29704  wwlksm1edg  29910  wwlksnred  29921  clwlkclwwlklem2  30028  clwwlkinwwlk  30068  clwwlkf  30075  wwlksubclwwlk  30086  occon  31315  xrge0infss  32770  resspos  32940  resstos  32941  gsummptres2  33038  submarchi  33175  prmidl2  33448  sigaclci  34112  measiun  34198  elmbfmvol2  34248  sibfof  34321  ftc2re  34591  bnj1118  34976  subfacp1lem3  35166  iccllysconn  35234  dmopab3rexdif  35389  untint  35691  untangtr  35693  dfon2lem6  35769  dfon2lem8  35771  dfon2lem9  35772  neibastop1  36341  neibastop2lem  36342  neibastop3  36344  weiunse  36450  finixpnum  37591  ptrecube  37606  poimirlem26  37632  poimirlem27  37633  poimirlem30  37636  heicant  37641  volsupnfl  37651  prdstotbnd  37780  heibor1lem  37795  ispridl2  38024  deg1gprod  42121  elrfirn2  42683  rabdiophlem1  42788  dford3lem1  43014  kelac1  43051  ssralv2  44528  ssralv2VD  44863  climinf  45561  limsupvaluz2  45693  supcnvlimsup  45695  iccpartres  47342  uhgrimisgrgric  47836