Theorem ssralv 4048

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

Syntax hints:   → wi 4  ∀wal 1532   ∈ wcel 2099  ∀wral 3051   ⊆ wss 3947

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

This theorem depends on definitions:  df-bi 206  df-ral 3052  df-ss 3964

This theorem is referenced by:  ss2ralv  4050  intss  4977  iinss1  5016  disjiun  5140  poss  5596  sess2  5651  isores3  7347  isoini2  7351  xpord2indlem  8161  xpord3inddlem  8168  poseq  8172  soseq  8173  smores  8382  smores2  8384  tfrlem5  8410  naddssim  8715  resixp  8962  ac6sfi  9321  iunfi  9385  ixpfi2  9394  marypha1lem  9476  ordtypelem2  9562  ttrclselem2  9769  tcrank  9927  acndom  10094  pwsdompw  10247  ssfin3ds  10373  fin1a2s  10457  hsmexlem4  10472  domtriomlem  10485  zornn0g  10548  fpwwe2lem12  10685  ingru  10858  cshw1  14830  rexanuz  15350  cau3lem  15359  caubnd  15363  limsupgord  15474  limsupval2  15482  rlimres  15560  lo1res  15561  o1of2  15615  o1rlimmul  15621  climsup  15674  fsumiun  15825  lcmfunsnlem1  16638  coprmprod  16662  pcfac  16901  vdwnnlem2  16998  firest  17447  imasaddfnlem  17543  imasvscafn  17552  psss  18605  tsrss  18614  cntz2ss  19329  cntzmhm2  19336  subgpgp  19595  efgsres  19736  telgsumfzs  19987  telgsums  19991  dprdss  20029  acsfn1p  20778  ocv2ss  21669  mretopd  23087  tgcn  23247  tgcnp  23248  subbascn  23249  cnss2  23272  cncnp  23275  sslm  23294  t1ficld  23322  tgcmp  23396  1stcfb  23440  islly2  23479  dislly  23492  comppfsc  23527  ptbasfi  23576  ptcnplem  23616  tx1stc  23645  qtoptop2  23694  fbunfip  23864  flftg  23991  txflf  24001  fclsbas  24016  fclsss1  24017  fclsss2  24018  alexsubb  24041  tmdgsum2  24091  metrest  24524  rescncf  24908  cnllycmp  24973  bndth  24975  fgcfil  25290  ivthlem2  25472  ivthlem3  25473  ovolsslem  25504  ovolfiniun  25521  finiunmbl  25564  volfiniun  25567  iunmbl  25573  ioombl1lem4  25581  dyadmax  25618  vitali  25633  mbfimaopnlem  25675  mbflimsup  25686  mbfi1flim  25744  ditgeq3  25870  dvferm  26011  rollelem  26012  dvivthlem1  26032  itgsubstlem  26074  aalioulem2  26361  ulmcaulem  26423  ulmss  26426  xrlimcnp  26996  2sqreunnlem2  27484  pntlem3  27638  pntlemp  27639  pntleml  27640  nosepon  27695  noresle  27727  sssslt1  27825  sssslt2  27826  uspgr2wlkeq  29583  redwlk  29609  wwlksm1edg  29815  wwlksnred  29826  clwlkclwwlklem2  29933  clwwlkinwwlk  29973  clwwlkf  29980  wwlksubclwwlk  29991  occon  31220  xrge0infss  32664  resspos  32836  resstos  32837  gsummptres2  32921  submarchi  33051  prmidl2  33316  sigaclci  33965  measiun  34051  elmbfmvol2  34101  sibfof  34174  ftc2re  34444  bnj1118  34829  subfacp1lem3  35010  iccllysconn  35078  dmopab3rexdif  35233  untint  35534  untangtr  35536  dfon2lem6  35612  dfon2lem8  35614  dfon2lem9  35615  neibastop1  36071  neibastop2lem  36072  neibastop3  36074  finixpnum  37306  ptrecube  37321  poimirlem26  37347  poimirlem27  37348  poimirlem30  37351  heicant  37356  volsupnfl  37366  prdstotbnd  37495  heibor1lem  37510  ispridl2  37739  deg1gprod  41838  elrfirn2  42353  rabdiophlem1  42458  dford3lem1  42684  kelac1  42724  ssralv2  44207  ssralv2VD  44542  climinf  45227  limsupvaluz2  45359  supcnvlimsup  45361  iccpartres  46990  uhgrimisgrgric  47478