Theorem ssralv 4077

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2108  ∀wral 3067   ⊆ wss 3976

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

This theorem depends on definitions:  df-bi 207  df-ral 3068  df-ss 3993

This theorem is referenced by:  ss2ralv  4079  intss  4993  iinss1  5030  disjiun  5154  poss  5609  sess2  5666  isores3  7371  isoini2  7375  xpord2indlem  8188  xpord3inddlem  8195  poseq  8199  soseq  8200  smores  8408  smores2  8410  tfrlem5  8436  naddssim  8741  resixp  8991  ac6sfi  9348  iunfi  9411  ixpfi2  9420  marypha1lem  9502  ordtypelem2  9588  ttrclselem2  9795  tcrank  9953  acndom  10120  pwsdompw  10272  ssfin3ds  10399  fin1a2s  10483  hsmexlem4  10498  domtriomlem  10511  zornn0g  10574  fpwwe2lem12  10711  ingru  10884  cshw1  14870  rexanuz  15394  cau3lem  15403  caubnd  15407  limsupgord  15518  limsupval2  15526  rlimres  15604  lo1res  15605  o1of2  15659  o1rlimmul  15665  climsup  15718  fsumiun  15869  lcmfunsnlem1  16684  coprmprod  16708  pcfac  16946  vdwnnlem2  17043  firest  17492  imasaddfnlem  17588  imasvscafn  17597  psss  18650  tsrss  18659  cntz2ss  19375  cntzmhm2  19382  subgpgp  19639  efgsres  19780  telgsumfzs  20031  telgsums  20035  dprdss  20073  acsfn1p  20822  ocv2ss  21714  mretopd  23121  tgcn  23281  tgcnp  23282  subbascn  23283  cnss2  23306  cncnp  23309  sslm  23328  t1ficld  23356  tgcmp  23430  1stcfb  23474  islly2  23513  dislly  23526  comppfsc  23561  ptbasfi  23610  ptcnplem  23650  tx1stc  23679  qtoptop2  23728  fbunfip  23898  flftg  24025  txflf  24035  fclsbas  24050  fclsss1  24051  fclsss2  24052  alexsubb  24075  tmdgsum2  24125  metrest  24558  rescncf  24942  cnllycmp  25007  bndth  25009  fgcfil  25324  ivthlem2  25506  ivthlem3  25507  ovolsslem  25538  ovolfiniun  25555  finiunmbl  25598  volfiniun  25601  iunmbl  25607  ioombl1lem4  25615  dyadmax  25652  vitali  25667  mbfimaopnlem  25709  mbflimsup  25720  mbfi1flim  25778  ditgeq3  25905  dvferm  26046  rollelem  26047  dvivthlem1  26067  itgsubstlem  26109  aalioulem2  26393  ulmcaulem  26455  ulmss  26458  xrlimcnp  27029  2sqreunnlem2  27517  pntlem3  27671  pntlemp  27672  pntleml  27673  nosepon  27728  noresle  27760  sssslt1  27858  sssslt2  27859  uspgr2wlkeq  29682  redwlk  29708  wwlksm1edg  29914  wwlksnred  29925  clwlkclwwlklem2  30032  clwwlkinwwlk  30072  clwwlkf  30079  wwlksubclwwlk  30090  occon  31319  xrge0infss  32767  resspos  32939  resstos  32940  gsummptres2  33036  submarchi  33166  prmidl2  33434  sigaclci  34096  measiun  34182  elmbfmvol2  34232  sibfof  34305  ftc2re  34575  bnj1118  34960  subfacp1lem3  35150  iccllysconn  35218  dmopab3rexdif  35373  untint  35674  untangtr  35676  dfon2lem6  35752  dfon2lem8  35754  dfon2lem9  35755  neibastop1  36325  neibastop2lem  36326  neibastop3  36328  weiunse  36434  finixpnum  37565  ptrecube  37580  poimirlem26  37606  poimirlem27  37607  poimirlem30  37610  heicant  37615  volsupnfl  37625  prdstotbnd  37754  heibor1lem  37769  ispridl2  37998  deg1gprod  42097  elrfirn2  42652  rabdiophlem1  42757  dford3lem1  42983  kelac1  43020  ssralv2  44502  ssralv2VD  44837  climinf  45527  limsupvaluz2  45659  supcnvlimsup  45661  iccpartres  47292  uhgrimisgrgric  47783