Theorem ssralv 4014

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 3930	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		imim1 84	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1842	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)))
4		df-ral 3086	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
5		df-ral 3086	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))
7	1, 6	sylbi 220	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4  ∀wal 1565   ∈ wcel 2149  ∀wral 3085   ⊆ wss 3913

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

This theorem depends on definitions:  df-bi 210  df-ral 3086  df-ss 3930

This theorem is referenced by:  ss2ralv  4016  intss  4935  iinss1  4973  disjiun  5098  poss  5569  sess2  5625  isores3  7331  isoini2  7335  xpord2indlem  8139  xpord3inddlem  8146  poseq  8150  soseq  8151  smores  8335  smores2  8337  tfrlem5  8362  naddssim  8668  resixp  8927  ac6sfi  9240  iunfi  9296  ixpfi2  9303  marypha1lem  9389  ordtypelem2  9477  ttrclselem2  9691  tcrank  9852  acndom  10031  pwsdompw  10182  ssfin3ds  10310  fin1a2s  10394  hsmexlem4  10409  domtriomlem  10422  zornn0g  10485  fpwwe2lem12  10623  ingru  10796  cshw1  14855  rexanuz  15393  cau3lem  15402  caubnd  15406  limsupgord  15519  limsupval2  15527  rlimres  15605  lo1res  15606  o1of2  15660  o1rlimmul  15666  climsup  15717  fsumiun  15869  lcmfunsnlem1  16691  coprmprod  16715  pcfac  16955  vdwnnlem2  17052  firest  17481  imasaddfnlem  17578  imasvscafn  17587  resspos  18481  resstos  18482  psss  18632  tsrss  18641  cntz2ss  19401  cntzmhm2  19408  subgpgp  19663  efgsres  19804  telgsumfzs  20055  telgsums  20059  dprdss  20097  acsfn1p  20876  prmidl2  21433  ocv2ss  21788  mretopd  23214  tgcn  23374  tgcnp  23375  subbascn  23376  cnss2  23399  cncnp  23402  sslm  23421  t1ficld  23449  tgcmp  23523  1stcfb  23567  islly2  23606  dislly  23619  comppfsc  23654  ptbasfi  23703  ptcnplem  23743  tx1stc  23772  qtoptop2  23821  fbunfip  23991  flftg  24118  txflf  24128  fclsbas  24143  fclsss1  24144  fclsss2  24145  alexsubb  24168  tmdgsum2  24218  metrest  24646  rescncf  25021  cnllycmp  25080  bndth  25082  fgcfil  25395  ivthlem2  25576  ivthlem3  25577  ovolsslem  25608  ovolfiniun  25625  finiunmbl  25668  volfiniun  25671  iunmbl  25677  ioombl1lem4  25685  dyadmax  25722  vitali  25737  mbfimaopnlem  25779  mbflimsup  25790  mbfi1flim  25847  ditgeq3  25974  dvferm  26112  rollelem  26113  dvivthlem1  26132  itgsubstlem  26172  aalioulem2  26459  ulmcaulem  26519  ulmss  26522  xrlimcnp  27095  2sqreunnlem2  27581  pntlem3  27735  pntlemp  27736  pntleml  27737  nosepon  27791  noresle  27823  ssslts1  27928  ssslts2  27929  uspgr2wlkeq  29932  redwlk  29957  wwlksm1edg  30167  wwlksnred  30178  clwlkclwwlklem2  30288  clwwlkinwwlk  30328  clwwlkf  30335  wwlksubclwwlk  30346  occon  31576  xrge0infss  33042  gsummptres2  33310  submarchi  33443  sigaclci  34463  measiun  34549  elmbfmvol2  34598  sibfof  34671  ftc2re  34926  bnj1118  35313  subfacp1lem3  35569  iccllysconn  35637  dmopab3rexdif  35792  untint  36099  untangtr  36101  dfon2lem6  36173  dfon2lem8  36175  dfon2lem9  36176  neibastop1  36755  neibastop2lem  36756  neibastop3  36758  weiunse  36864  finixpnum  38139  ptrecube  38154  poimirlem26  38180  poimirlem27  38181  poimirlem30  38184  heicant  38189  volsupnfl  38199  prdstotbnd  38328  heibor1lem  38343  ispridl2  38572  deg1gprod  42792  elrfirn2  43314  rabdiophlem1  43415  dford3lem1  43640  kelac1  43677  ssralv2  45127  ssralv2VD  45461  climinf  46209  limsupvaluz2  46339  supcnvlimsup  46341  iccpartres  48051  uhgrimisgrgric  48580  termc  50177