Theorem ssralv 4052

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108  ∀wral 3061   ⊆ wss 3951

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 3062  df-ss 3968

This theorem is referenced by:  ss2ralv  4054  intss  4969  iinss1  5007  disjiun  5131  poss  5594  sess2  5651  isores3  7355  isoini2  7359  xpord2indlem  8172  xpord3inddlem  8179  poseq  8183  soseq  8184  smores  8392  smores2  8394  tfrlem5  8420  naddssim  8723  resixp  8973  ac6sfi  9320  iunfi  9383  ixpfi2  9390  marypha1lem  9473  ordtypelem2  9559  ttrclselem2  9766  tcrank  9924  acndom  10091  pwsdompw  10243  ssfin3ds  10370  fin1a2s  10454  hsmexlem4  10469  domtriomlem  10482  zornn0g  10545  fpwwe2lem12  10682  ingru  10855  cshw1  14860  rexanuz  15384  cau3lem  15393  caubnd  15397  limsupgord  15508  limsupval2  15516  rlimres  15594  lo1res  15595  o1of2  15649  o1rlimmul  15655  climsup  15706  fsumiun  15857  lcmfunsnlem1  16674  coprmprod  16698  pcfac  16937  vdwnnlem2  17034  firest  17477  imasaddfnlem  17573  imasvscafn  17582  psss  18625  tsrss  18634  cntz2ss  19353  cntzmhm2  19360  subgpgp  19615  efgsres  19756  telgsumfzs  20007  telgsums  20011  dprdss  20049  acsfn1p  20800  ocv2ss  21691  mretopd  23100  tgcn  23260  tgcnp  23261  subbascn  23262  cnss2  23285  cncnp  23288  sslm  23307  t1ficld  23335  tgcmp  23409  1stcfb  23453  islly2  23492  dislly  23505  comppfsc  23540  ptbasfi  23589  ptcnplem  23629  tx1stc  23658  qtoptop2  23707  fbunfip  23877  flftg  24004  txflf  24014  fclsbas  24029  fclsss1  24030  fclsss2  24031  alexsubb  24054  tmdgsum2  24104  metrest  24537  rescncf  24923  cnllycmp  24988  bndth  24990  fgcfil  25305  ivthlem2  25487  ivthlem3  25488  ovolsslem  25519  ovolfiniun  25536  finiunmbl  25579  volfiniun  25582  iunmbl  25588  ioombl1lem4  25596  dyadmax  25633  vitali  25648  mbfimaopnlem  25690  mbflimsup  25701  mbfi1flim  25758  ditgeq3  25885  dvferm  26026  rollelem  26027  dvivthlem1  26047  itgsubstlem  26089  aalioulem2  26375  ulmcaulem  26437  ulmss  26440  xrlimcnp  27011  2sqreunnlem2  27499  pntlem3  27653  pntlemp  27654  pntleml  27655  nosepon  27710  noresle  27742  sssslt1  27840  sssslt2  27841  uspgr2wlkeq  29664  redwlk  29690  wwlksm1edg  29901  wwlksnred  29912  clwlkclwwlklem2  30019  clwwlkinwwlk  30059  clwwlkf  30066  wwlksubclwwlk  30077  occon  31306  xrge0infss  32764  resspos  32956  resstos  32957  gsummptres2  33056  submarchi  33193  prmidl2  33469  sigaclci  34133  measiun  34219  elmbfmvol2  34269  sibfof  34342  ftc2re  34613  bnj1118  34998  subfacp1lem3  35187  iccllysconn  35255  dmopab3rexdif  35410  untint  35712  untangtr  35714  dfon2lem6  35789  dfon2lem8  35791  dfon2lem9  35792  neibastop1  36360  neibastop2lem  36361  neibastop3  36363  weiunse  36469  finixpnum  37612  ptrecube  37627  poimirlem26  37653  poimirlem27  37654  poimirlem30  37657  heicant  37662  volsupnfl  37672  prdstotbnd  37801  heibor1lem  37816  ispridl2  38045  deg1gprod  42141  elrfirn2  42707  rabdiophlem1  42812  dford3lem1  43038  kelac1  43075  ssralv2  44551  ssralv2VD  44886  climinf  45621  limsupvaluz2  45753  supcnvlimsup  45755  iccpartres  47405  uhgrimisgrgric  47899  termc  49149