Theorem ssralv 3990

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 3906	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		imim1 83	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1817	. . 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 1540   ∈ wcel 2114  ∀wral 3051   ⊆ wss 3889

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

This theorem depends on definitions:  df-bi 207  df-ral 3052  df-ss 3906

This theorem is referenced by:  ss2ralv  3992  intss  4911  iinss1  4949  disjiun  5073  poss  5541  sess2  5597  isores3  7290  isoini2  7294  xpord2indlem  8097  xpord3inddlem  8104  poseq  8108  soseq  8109  smores  8292  smores2  8294  tfrlem5  8319  naddssim  8621  resixp  8881  ac6sfi  9194  iunfi  9253  ixpfi2  9260  marypha1lem  9346  ordtypelem2  9434  ttrclselem2  9647  tcrank  9808  acndom  9973  pwsdompw  10125  ssfin3ds  10252  fin1a2s  10336  hsmexlem4  10351  domtriomlem  10364  zornn0g  10427  fpwwe2lem12  10565  ingru  10738  cshw1  14784  rexanuz  15308  cau3lem  15317  caubnd  15321  limsupgord  15434  limsupval2  15442  rlimres  15520  lo1res  15521  o1of2  15575  o1rlimmul  15581  climsup  15632  fsumiun  15784  lcmfunsnlem1  16606  coprmprod  16630  pcfac  16870  vdwnnlem2  16967  firest  17395  imasaddfnlem  17492  imasvscafn  17501  resspos  18395  resstos  18396  psss  18546  tsrss  18555  cntz2ss  19310  cntzmhm2  19317  subgpgp  19572  efgsres  19713  telgsumfzs  19964  telgsums  19968  dprdss  20006  acsfn1p  20776  ocv2ss  21653  mretopd  23057  tgcn  23217  tgcnp  23218  subbascn  23219  cnss2  23242  cncnp  23245  sslm  23264  t1ficld  23292  tgcmp  23366  1stcfb  23410  islly2  23449  dislly  23462  comppfsc  23497  ptbasfi  23546  ptcnplem  23586  tx1stc  23615  qtoptop2  23664  fbunfip  23834  flftg  23961  txflf  23971  fclsbas  23986  fclsss1  23987  fclsss2  23988  alexsubb  24011  tmdgsum2  24061  metrest  24489  rescncf  24864  cnllycmp  24923  bndth  24925  fgcfil  25238  ivthlem2  25419  ivthlem3  25420  ovolsslem  25451  ovolfiniun  25468  finiunmbl  25511  volfiniun  25514  iunmbl  25520  ioombl1lem4  25528  dyadmax  25565  vitali  25580  mbfimaopnlem  25622  mbflimsup  25633  mbfi1flim  25690  ditgeq3  25817  dvferm  25955  rollelem  25956  dvivthlem1  25975  itgsubstlem  26015  aalioulem2  26299  ulmcaulem  26359  ulmss  26362  xrlimcnp  26932  2sqreunnlem2  27418  pntlem3  27572  pntlemp  27573  pntleml  27574  nosepon  27629  noresle  27661  ssslts1  27765  ssslts2  27766  uspgr2wlkeq  29714  redwlk  29739  wwlksm1edg  29949  wwlksnred  29960  clwlkclwwlklem2  30070  clwwlkinwwlk  30110  clwwlkf  30117  wwlksubclwwlk  30128  occon  31358  xrge0infss  32833  gsummptres2  33114  submarchi  33247  prmidl2  33501  sigaclci  34276  measiun  34362  elmbfmvol2  34411  sibfof  34484  ftc2re  34742  bnj1118  35126  subfacp1lem3  35364  iccllysconn  35432  dmopab3rexdif  35587  untint  35894  untangtr  35896  dfon2lem6  35968  dfon2lem8  35970  dfon2lem9  35971  neibastop1  36541  neibastop2lem  36542  neibastop3  36544  weiunse  36650  finixpnum  37926  ptrecube  37941  poimirlem26  37967  poimirlem27  37968  poimirlem30  37971  heicant  37976  volsupnfl  37986  prdstotbnd  38115  heibor1lem  38130  ispridl2  38359  deg1gprod  42579  elrfirn2  43128  rabdiophlem1  43229  dford3lem1  43454  kelac1  43491  ssralv2  44958  ssralv2VD  45292  climinf  46036  limsupvaluz2  46166  supcnvlimsup  46168  iccpartres  47878  uhgrimisgrgric  48407  termc  49994