Theorem ssralv 3998

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  ∀wral 3047   ⊆ wss 3897

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

This theorem depends on definitions:  df-bi 207  df-ral 3048  df-ss 3914

This theorem is referenced by:  ss2ralv  4000  intss  4914  iinss1  4952  disjiun  5074  poss  5521  sess2  5577  isores3  7264  isoini2  7268  xpord2indlem  8072  xpord3inddlem  8079  poseq  8083  soseq  8084  smores  8267  smores2  8269  tfrlem5  8294  naddssim  8595  resixp  8852  ac6sfi  9163  iunfi  9222  ixpfi2  9229  marypha1lem  9312  ordtypelem2  9400  ttrclselem2  9611  tcrank  9772  acndom  9937  pwsdompw  10089  ssfin3ds  10216  fin1a2s  10300  hsmexlem4  10315  domtriomlem  10328  zornn0g  10391  fpwwe2lem12  10528  ingru  10701  cshw1  14724  rexanuz  15248  cau3lem  15257  caubnd  15261  limsupgord  15374  limsupval2  15382  rlimres  15460  lo1res  15461  o1of2  15515  o1rlimmul  15521  climsup  15572  fsumiun  15723  lcmfunsnlem1  16543  coprmprod  16567  pcfac  16806  vdwnnlem2  16903  firest  17331  imasaddfnlem  17427  imasvscafn  17436  resspos  18330  resstos  18331  psss  18481  tsrss  18490  cntz2ss  19242  cntzmhm2  19249  subgpgp  19504  efgsres  19645  telgsumfzs  19896  telgsums  19900  dprdss  19938  acsfn1p  20709  ocv2ss  21605  mretopd  23002  tgcn  23162  tgcnp  23163  subbascn  23164  cnss2  23187  cncnp  23190  sslm  23209  t1ficld  23237  tgcmp  23311  1stcfb  23355  islly2  23394  dislly  23407  comppfsc  23442  ptbasfi  23491  ptcnplem  23531  tx1stc  23560  qtoptop2  23609  fbunfip  23779  flftg  23906  txflf  23916  fclsbas  23931  fclsss1  23932  fclsss2  23933  alexsubb  23956  tmdgsum2  24006  metrest  24434  rescncf  24812  cnllycmp  24877  bndth  24879  fgcfil  25193  ivthlem2  25375  ivthlem3  25376  ovolsslem  25407  ovolfiniun  25424  finiunmbl  25467  volfiniun  25470  iunmbl  25476  ioombl1lem4  25484  dyadmax  25521  vitali  25536  mbfimaopnlem  25578  mbflimsup  25589  mbfi1flim  25646  ditgeq3  25773  dvferm  25914  rollelem  25915  dvivthlem1  25935  itgsubstlem  25977  aalioulem2  26263  ulmcaulem  26325  ulmss  26328  xrlimcnp  26900  2sqreunnlem2  27388  pntlem3  27542  pntlemp  27543  pntleml  27544  nosepon  27599  noresle  27631  sssslt1  27731  sssslt2  27732  uspgr2wlkeq  29619  redwlk  29644  wwlksm1edg  29854  wwlksnred  29865  clwlkclwwlklem2  29972  clwwlkinwwlk  30012  clwwlkf  30019  wwlksubclwwlk  30030  occon  31259  xrge0infss  32735  gsummptres2  33025  submarchi  33147  prmidl2  33398  sigaclci  34137  measiun  34223  elmbfmvol2  34272  sibfof  34345  ftc2re  34603  bnj1118  34988  subfacp1lem3  35218  iccllysconn  35286  dmopab3rexdif  35441  untint  35748  untangtr  35750  dfon2lem6  35822  dfon2lem8  35824  dfon2lem9  35825  neibastop1  36393  neibastop2lem  36394  neibastop3  36396  weiunse  36502  finixpnum  37645  ptrecube  37660  poimirlem26  37686  poimirlem27  37687  poimirlem30  37690  heicant  37695  volsupnfl  37705  prdstotbnd  37834  heibor1lem  37849  ispridl2  38078  deg1gprod  42173  elrfirn2  42729  rabdiophlem1  42834  dford3lem1  43059  kelac1  43096  ssralv2  44564  ssralv2VD  44898  climinf  45646  limsupvaluz2  45776  supcnvlimsup  45778  iccpartres  47449  uhgrimisgrgric  47962  termc  49551