Theorem ssralv 4002

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  ∀wral 3051   ⊆ wss 3901

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 3052  df-ss 3918

This theorem is referenced by:  ss2ralv  4004  intss  4924  iinss1  4962  disjiun  5086  poss  5534  sess2  5590  isores3  7281  isoini2  7285  xpord2indlem  8089  xpord3inddlem  8096  poseq  8100  soseq  8101  smores  8284  smores2  8286  tfrlem5  8311  naddssim  8613  resixp  8871  ac6sfi  9184  iunfi  9243  ixpfi2  9250  marypha1lem  9336  ordtypelem2  9424  ttrclselem2  9635  tcrank  9796  acndom  9961  pwsdompw  10113  ssfin3ds  10240  fin1a2s  10324  hsmexlem4  10339  domtriomlem  10352  zornn0g  10415  fpwwe2lem12  10553  ingru  10726  cshw1  14745  rexanuz  15269  cau3lem  15278  caubnd  15282  limsupgord  15395  limsupval2  15403  rlimres  15481  lo1res  15482  o1of2  15536  o1rlimmul  15542  climsup  15593  fsumiun  15744  lcmfunsnlem1  16564  coprmprod  16588  pcfac  16827  vdwnnlem2  16924  firest  17352  imasaddfnlem  17449  imasvscafn  17458  resspos  18352  resstos  18353  psss  18503  tsrss  18512  cntz2ss  19264  cntzmhm2  19271  subgpgp  19526  efgsres  19667  telgsumfzs  19918  telgsums  19922  dprdss  19960  acsfn1p  20732  ocv2ss  21628  mretopd  23036  tgcn  23196  tgcnp  23197  subbascn  23198  cnss2  23221  cncnp  23224  sslm  23243  t1ficld  23271  tgcmp  23345  1stcfb  23389  islly2  23428  dislly  23441  comppfsc  23476  ptbasfi  23525  ptcnplem  23565  tx1stc  23594  qtoptop2  23643  fbunfip  23813  flftg  23940  txflf  23950  fclsbas  23965  fclsss1  23966  fclsss2  23967  alexsubb  23990  tmdgsum2  24040  metrest  24468  rescncf  24846  cnllycmp  24911  bndth  24913  fgcfil  25227  ivthlem2  25409  ivthlem3  25410  ovolsslem  25441  ovolfiniun  25458  finiunmbl  25501  volfiniun  25504  iunmbl  25510  ioombl1lem4  25518  dyadmax  25555  vitali  25570  mbfimaopnlem  25612  mbflimsup  25623  mbfi1flim  25680  ditgeq3  25807  dvferm  25948  rollelem  25949  dvivthlem1  25969  itgsubstlem  26011  aalioulem2  26297  ulmcaulem  26359  ulmss  26362  xrlimcnp  26934  2sqreunnlem2  27422  pntlem3  27576  pntlemp  27577  pntleml  27578  nosepon  27633  noresle  27665  ssslts1  27769  ssslts2  27770  uspgr2wlkeq  29719  redwlk  29744  wwlksm1edg  29954  wwlksnred  29965  clwlkclwwlklem2  30075  clwwlkinwwlk  30115  clwwlkf  30122  wwlksubclwwlk  30133  occon  31362  xrge0infss  32840  gsummptres2  33136  submarchi  33268  prmidl2  33522  sigaclci  34289  measiun  34375  elmbfmvol2  34424  sibfof  34497  ftc2re  34755  bnj1118  35140  subfacp1lem3  35376  iccllysconn  35444  dmopab3rexdif  35599  untint  35906  untangtr  35908  dfon2lem6  35980  dfon2lem8  35982  dfon2lem9  35983  neibastop1  36553  neibastop2lem  36554  neibastop3  36556  weiunse  36662  finixpnum  37806  ptrecube  37821  poimirlem26  37847  poimirlem27  37848  poimirlem30  37851  heicant  37856  volsupnfl  37866  prdstotbnd  37995  heibor1lem  38010  ispridl2  38239  deg1gprod  42394  elrfirn2  42938  rabdiophlem1  43043  dford3lem1  43268  kelac1  43305  ssralv2  44772  ssralv2VD  45106  climinf  45852  limsupvaluz2  45982  supcnvlimsup  45984  iccpartres  47664  uhgrimisgrgric  48177  termc  49764