Theorem ssralv 4007

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2146  ∀wral 3081   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3082  df-ss 3923

This theorem is used by:  ss2ralv  4009  intss  4936  iinss1  4974  disjiun  5099  poss  5573  sess2  5629  isores3  7339  isoini2  7343  xpord2indlem  8145  xpord3inddlem  8152  poseq  8156  soseq  8157  smores  8341  smores2  8343  tfrlem5  8368  naddssim  8674  resixp  8933  ac6sfi  9247  iunfi  9303  ixpfi2  9310  marypha1lem  9396  ordtypelem2  9484  ttrclselem2  9698  tcrank  9859  acndom  10047  pwsdompw  10198  ssfin3ds  10325  fin1a2s  10409  hsmexlem4  10424  domtriomlem  10437  zornn0g  10500  fpwwe2lem12  10638  ingru  10811  cshw1  14879  rexanuz  15417  cau3lem  15426  caubnd  15430  limsupgord  15543  limsupval2  15551  rlimres  15629  lo1res  15630  o1of2  15684  o1rlimmul  15690  climsup  15741  fsumiun  15892  lcmfunsnlem1  16713  coprmprod  16737  pcfac  16977  vdwnnlem2  17074  firest  17503  imasaddfnlem  17600  imasvscafn  17609  resspos  18503  resstos  18504  psss  18654  tsrss  18663  idressidex0  18753  idressid  18755  cntz2ss  19429  cntzmhm2  19436  subgpgp  19691  efgsres  19832  telgsumfzs  20083  telgsums  20087  dprdss  20125  acsfn1p  20932  prmidl2  21496  ocv2ss  21853  mretopd  23279  tgcn  23439  tgcnp  23440  subbascn  23441  cnss2  23464  cncnp  23467  sslm  23486  t1ficld  23514  tgcmp  23588  1stcfb  23632  islly2  23672  dislly  23685  comppfsc  23720  ptbasfi  23769  ptcnplem  23809  tx1stc  23838  qtoptop2  23887  fbunfip  24057  flftg  24184  txflf  24194  fclsbas  24209  fclsss1  24210  fclsss2  24211  alexsubb  24234  tmdgsum2  24284  metrest  24712  rescncf  25087  cnllycmp  25146  bndth  25148  fgcfil  25461  ivthlem2  25642  ivthlem3  25643  ovolsslem  25674  ovolfiniun  25691  finiunmbl  25734  volfiniun  25737  iunmbl  25743  ioombl1lem4  25751  dyadmax  25788  vitali  25803  mbfimaopnlem  25845  mbflimsup  25856  mbfi1flim  25913  ditgeq3  26040  dvferm  26178  rollelem  26179  dvivthlem1  26198  itgsubstlem  26238  aalioulem2  26527  ulmcaulem  26588  ulmss  26591  xrlimcnp  27164  2sqreunnlem2  27650  pntlem3  27804  pntlemp  27805  pntleml  27806  nosepon  27860  noresle  27892  ssslts1  27997  ssslts2  27998  uspgr2wlkeq  30029  redwlk  30054  wwlksm1edg  30273  wwlksnred  30284  clwlkclwwlklem2  30394  clwwlkinwwlk  30434  clwwlkf  30441  wwlksubclwwlk  30452  occon  31686  xrge0infss  33151  gsummptres2  33413  submarchi  33546  sigaclci  34562  measiun  34649  elmbfmvol2  34698  sibfof  34771  ftc2re  35026  bnj1118  35413  subfacp1lem3  35687  iccllysconn  35755  dmopab3rexdif  35910  untint  36217  untangtr  36219  dfon2lem6  36291  dfon2lem8  36293  dfon2lem9  36294  neibastop1  36903  neibastop2lem  36904  neibastop3  36906  weiunse  37012  finixpnum  38289  ptrecube  38304  poimirlem26  38330  poimirlem27  38331  poimirlem30  38334  heicant  38339  volsupnfl  38349  prdstotbnd  38478  heibor1lem  38493  ispridl2  38722  deg1gprod  42940  elrfirn2  43460  rabdiophlem1  43561  dford3lem1  43786  kelac1  43823  ssralv2  45273  ssralv2VD  45607  climinf  46355  limsupvaluz2  46485  supcnvlimsup  46487  iccpartres  48200  uhgrimisgrgric  48729  termc  50330