Theorem ssralv 4004

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 3920	. 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 3903

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 3920

This theorem is referenced by:  ss2ralv  4006  intss  4926  iinss1  4964  disjiun  5088  poss  5542  sess2  5598  isores3  7291  isoini2  7295  xpord2indlem  8099  xpord3inddlem  8106  poseq  8110  soseq  8111  smores  8294  smores2  8296  tfrlem5  8321  naddssim  8623  resixp  8883  ac6sfi  9196  iunfi  9255  ixpfi2  9262  marypha1lem  9348  ordtypelem2  9436  ttrclselem2  9647  tcrank  9808  acndom  9973  pwsdompw  10125  ssfin3ds  10252  fin1a2s  10336  hsmexlem4  10351  domtriomlem  10364  zornn0g  10427  fpwwe2lem12  10565  ingru  10738  cshw1  14757  rexanuz  15281  cau3lem  15290  caubnd  15294  limsupgord  15407  limsupval2  15415  rlimres  15493  lo1res  15494  o1of2  15548  o1rlimmul  15554  climsup  15605  fsumiun  15756  lcmfunsnlem1  16576  coprmprod  16600  pcfac  16839  vdwnnlem2  16936  firest  17364  imasaddfnlem  17461  imasvscafn  17470  resspos  18364  resstos  18365  psss  18515  tsrss  18524  cntz2ss  19276  cntzmhm2  19283  subgpgp  19538  efgsres  19679  telgsumfzs  19930  telgsums  19934  dprdss  19972  acsfn1p  20744  ocv2ss  21640  mretopd  23048  tgcn  23208  tgcnp  23209  subbascn  23210  cnss2  23233  cncnp  23236  sslm  23255  t1ficld  23283  tgcmp  23357  1stcfb  23401  islly2  23440  dislly  23453  comppfsc  23488  ptbasfi  23537  ptcnplem  23577  tx1stc  23606  qtoptop2  23655  fbunfip  23825  flftg  23952  txflf  23962  fclsbas  23977  fclsss1  23978  fclsss2  23979  alexsubb  24002  tmdgsum2  24052  metrest  24480  rescncf  24858  cnllycmp  24923  bndth  24925  fgcfil  25239  ivthlem2  25421  ivthlem3  25422  ovolsslem  25453  ovolfiniun  25470  finiunmbl  25513  volfiniun  25516  iunmbl  25522  ioombl1lem4  25530  dyadmax  25567  vitali  25582  mbfimaopnlem  25624  mbflimsup  25635  mbfi1flim  25692  ditgeq3  25819  dvferm  25960  rollelem  25961  dvivthlem1  25981  itgsubstlem  26023  aalioulem2  26309  ulmcaulem  26371  ulmss  26374  xrlimcnp  26946  2sqreunnlem2  27434  pntlem3  27588  pntlemp  27589  pntleml  27590  nosepon  27645  noresle  27677  ssslts1  27781  ssslts2  27782  uspgr2wlkeq  29731  redwlk  29756  wwlksm1edg  29966  wwlksnred  29977  clwlkclwwlklem2  30087  clwwlkinwwlk  30127  clwwlkf  30134  wwlksubclwwlk  30145  occon  31375  xrge0infss  32851  gsummptres2  33147  submarchi  33280  prmidl2  33534  sigaclci  34310  measiun  34396  elmbfmvol2  34445  sibfof  34518  ftc2re  34776  bnj1118  35160  subfacp1lem3  35398  iccllysconn  35466  dmopab3rexdif  35621  untint  35928  untangtr  35930  dfon2lem6  36002  dfon2lem8  36004  dfon2lem9  36005  neibastop1  36575  neibastop2lem  36576  neibastop3  36578  weiunse  36684  finixpnum  37856  ptrecube  37871  poimirlem26  37897  poimirlem27  37898  poimirlem30  37901  heicant  37906  volsupnfl  37916  prdstotbnd  38045  heibor1lem  38060  ispridl2  38289  deg1gprod  42510  elrfirn2  43053  rabdiophlem1  43158  dford3lem1  43383  kelac1  43420  ssralv2  44887  ssralv2VD  45221  climinf  45966  limsupvaluz2  46096  supcnvlimsup  46098  iccpartres  47778  uhgrimisgrgric  48291  termc  49878