Theorem ssralv 4032

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 3948	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		imim1 83	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1815	. . 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 1538   ∈ wcel 2109  ∀wral 3052   ⊆ wss 3931

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

This theorem depends on definitions:  df-bi 207  df-ral 3053  df-ss 3948

This theorem is referenced by:  ss2ralv  4034  intss  4950  iinss1  4988  disjiun  5112  poss  5568  sess2  5625  isores3  7333  isoini2  7337  xpord2indlem  8151  xpord3inddlem  8158  poseq  8162  soseq  8163  smores  8371  smores2  8373  tfrlem5  8399  naddssim  8702  resixp  8952  ac6sfi  9297  iunfi  9360  ixpfi2  9367  marypha1lem  9450  ordtypelem2  9538  ttrclselem2  9745  tcrank  9903  acndom  10070  pwsdompw  10222  ssfin3ds  10349  fin1a2s  10433  hsmexlem4  10448  domtriomlem  10461  zornn0g  10524  fpwwe2lem12  10661  ingru  10834  cshw1  14845  rexanuz  15369  cau3lem  15378  caubnd  15382  limsupgord  15493  limsupval2  15501  rlimres  15579  lo1res  15580  o1of2  15634  o1rlimmul  15640  climsup  15691  fsumiun  15842  lcmfunsnlem1  16661  coprmprod  16685  pcfac  16924  vdwnnlem2  17021  firest  17451  imasaddfnlem  17547  imasvscafn  17556  psss  18595  tsrss  18604  cntz2ss  19323  cntzmhm2  19330  subgpgp  19583  efgsres  19724  telgsumfzs  19975  telgsums  19979  dprdss  20017  acsfn1p  20764  ocv2ss  21638  mretopd  23035  tgcn  23195  tgcnp  23196  subbascn  23197  cnss2  23220  cncnp  23223  sslm  23242  t1ficld  23270  tgcmp  23344  1stcfb  23388  islly2  23427  dislly  23440  comppfsc  23475  ptbasfi  23524  ptcnplem  23564  tx1stc  23593  qtoptop2  23642  fbunfip  23812  flftg  23939  txflf  23949  fclsbas  23964  fclsss1  23965  fclsss2  23966  alexsubb  23989  tmdgsum2  24039  metrest  24468  rescncf  24846  cnllycmp  24911  bndth  24913  fgcfil  25228  ivthlem2  25410  ivthlem3  25411  ovolsslem  25442  ovolfiniun  25459  finiunmbl  25502  volfiniun  25505  iunmbl  25511  ioombl1lem4  25519  dyadmax  25556  vitali  25571  mbfimaopnlem  25613  mbflimsup  25624  mbfi1flim  25681  ditgeq3  25808  dvferm  25949  rollelem  25950  dvivthlem1  25970  itgsubstlem  26012  aalioulem2  26298  ulmcaulem  26360  ulmss  26363  xrlimcnp  26935  2sqreunnlem2  27423  pntlem3  27577  pntlemp  27578  pntleml  27579  nosepon  27634  noresle  27666  sssslt1  27764  sssslt2  27765  uspgr2wlkeq  29631  redwlk  29657  wwlksm1edg  29868  wwlksnred  29879  clwlkclwwlklem2  29986  clwwlkinwwlk  30026  clwwlkf  30033  wwlksubclwwlk  30044  occon  31273  xrge0infss  32742  resspos  32951  resstos  32952  gsummptres2  33052  submarchi  33189  prmidl2  33461  sigaclci  34168  measiun  34254  elmbfmvol2  34304  sibfof  34377  ftc2re  34635  bnj1118  35020  subfacp1lem3  35209  iccllysconn  35277  dmopab3rexdif  35432  untint  35734  untangtr  35736  dfon2lem6  35811  dfon2lem8  35813  dfon2lem9  35814  neibastop1  36382  neibastop2lem  36383  neibastop3  36385  weiunse  36491  finixpnum  37634  ptrecube  37649  poimirlem26  37675  poimirlem27  37676  poimirlem30  37679  heicant  37684  volsupnfl  37694  prdstotbnd  37823  heibor1lem  37838  ispridl2  38067  deg1gprod  42158  elrfirn2  42694  rabdiophlem1  42799  dford3lem1  43025  kelac1  43062  ssralv2  44531  ssralv2VD  44865  climinf  45615  limsupvaluz2  45747  supcnvlimsup  45749  iccpartres  47412  uhgrimisgrgric  47924  termc  49384