Theorem ssralv 3991

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3890

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 3053  df-ss 3907

This theorem is referenced by:  ss2ralv  3993  intss  4912  iinss1  4950  disjiun  5074  poss  5534  sess2  5590  isores3  7283  isoini2  7287  xpord2indlem  8090  xpord3inddlem  8097  poseq  8101  soseq  8102  smores  8285  smores2  8287  tfrlem5  8312  naddssim  8614  resixp  8874  ac6sfi  9187  iunfi  9246  ixpfi2  9253  marypha1lem  9339  ordtypelem2  9427  ttrclselem2  9638  tcrank  9799  acndom  9964  pwsdompw  10116  ssfin3ds  10243  fin1a2s  10327  hsmexlem4  10342  domtriomlem  10355  zornn0g  10418  fpwwe2lem12  10556  ingru  10729  cshw1  14775  rexanuz  15299  cau3lem  15308  caubnd  15312  limsupgord  15425  limsupval2  15433  rlimres  15511  lo1res  15512  o1of2  15566  o1rlimmul  15572  climsup  15623  fsumiun  15775  lcmfunsnlem1  16597  coprmprod  16621  pcfac  16861  vdwnnlem2  16958  firest  17386  imasaddfnlem  17483  imasvscafn  17492  resspos  18386  resstos  18387  psss  18537  tsrss  18546  cntz2ss  19301  cntzmhm2  19308  subgpgp  19563  efgsres  19704  telgsumfzs  19955  telgsums  19959  dprdss  19997  acsfn1p  20767  ocv2ss  21663  mretopd  23067  tgcn  23227  tgcnp  23228  subbascn  23229  cnss2  23252  cncnp  23255  sslm  23274  t1ficld  23302  tgcmp  23376  1stcfb  23420  islly2  23459  dislly  23472  comppfsc  23507  ptbasfi  23556  ptcnplem  23596  tx1stc  23625  qtoptop2  23674  fbunfip  23844  flftg  23971  txflf  23981  fclsbas  23996  fclsss1  23997  fclsss2  23998  alexsubb  24021  tmdgsum2  24071  metrest  24499  rescncf  24874  cnllycmp  24933  bndth  24935  fgcfil  25248  ivthlem2  25429  ivthlem3  25430  ovolsslem  25461  ovolfiniun  25478  finiunmbl  25521  volfiniun  25524  iunmbl  25530  ioombl1lem4  25538  dyadmax  25575  vitali  25590  mbfimaopnlem  25632  mbflimsup  25643  mbfi1flim  25700  ditgeq3  25827  dvferm  25965  rollelem  25966  dvivthlem1  25985  itgsubstlem  26025  aalioulem2  26310  ulmcaulem  26372  ulmss  26375  xrlimcnp  26945  2sqreunnlem2  27432  pntlem3  27586  pntlemp  27587  pntleml  27588  nosepon  27643  noresle  27675  ssslts1  27779  ssslts2  27780  uspgr2wlkeq  29729  redwlk  29754  wwlksm1edg  29964  wwlksnred  29975  clwlkclwwlklem2  30085  clwwlkinwwlk  30125  clwwlkf  30132  wwlksubclwwlk  30143  occon  31373  xrge0infss  32848  gsummptres2  33129  submarchi  33262  prmidl2  33516  sigaclci  34292  measiun  34378  elmbfmvol2  34427  sibfof  34500  ftc2re  34758  bnj1118  35142  subfacp1lem3  35380  iccllysconn  35448  dmopab3rexdif  35603  untint  35910  untangtr  35912  dfon2lem6  35984  dfon2lem8  35986  dfon2lem9  35987  neibastop1  36557  neibastop2lem  36558  neibastop3  36560  weiunse  36666  finixpnum  37940  ptrecube  37955  poimirlem26  37981  poimirlem27  37982  poimirlem30  37985  heicant  37990  volsupnfl  38000  prdstotbnd  38129  heibor1lem  38144  ispridl2  38373  deg1gprod  42593  elrfirn2  43142  rabdiophlem1  43247  dford3lem1  43472  kelac1  43509  ssralv2  44976  ssralv2VD  45310  climinf  46054  limsupvaluz2  46184  supcnvlimsup  46186  iccpartres  47890  uhgrimisgrgric  48419  termc  50006