Theorem ssralv 4015

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3914

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 3045  df-ss 3931

This theorem is referenced by:  ss2ralv  4017  intss  4933  iinss1  4971  disjiun  5095  poss  5548  sess2  5604  isores3  7310  isoini2  7314  xpord2indlem  8126  xpord3inddlem  8133  poseq  8137  soseq  8138  smores  8321  smores2  8323  tfrlem5  8348  naddssim  8649  resixp  8906  ac6sfi  9231  iunfi  9294  ixpfi2  9301  marypha1lem  9384  ordtypelem2  9472  ttrclselem2  9679  tcrank  9837  acndom  10004  pwsdompw  10156  ssfin3ds  10283  fin1a2s  10367  hsmexlem4  10382  domtriomlem  10395  zornn0g  10458  fpwwe2lem12  10595  ingru  10768  cshw1  14787  rexanuz  15312  cau3lem  15321  caubnd  15325  limsupgord  15438  limsupval2  15446  rlimres  15524  lo1res  15525  o1of2  15579  o1rlimmul  15585  climsup  15636  fsumiun  15787  lcmfunsnlem1  16607  coprmprod  16631  pcfac  16870  vdwnnlem2  16967  firest  17395  imasaddfnlem  17491  imasvscafn  17500  psss  18539  tsrss  18548  cntz2ss  19267  cntzmhm2  19274  subgpgp  19527  efgsres  19668  telgsumfzs  19919  telgsums  19923  dprdss  19961  acsfn1p  20708  ocv2ss  21582  mretopd  22979  tgcn  23139  tgcnp  23140  subbascn  23141  cnss2  23164  cncnp  23167  sslm  23186  t1ficld  23214  tgcmp  23288  1stcfb  23332  islly2  23371  dislly  23384  comppfsc  23419  ptbasfi  23468  ptcnplem  23508  tx1stc  23537  qtoptop2  23586  fbunfip  23756  flftg  23883  txflf  23893  fclsbas  23908  fclsss1  23909  fclsss2  23910  alexsubb  23933  tmdgsum2  23983  metrest  24412  rescncf  24790  cnllycmp  24855  bndth  24857  fgcfil  25171  ivthlem2  25353  ivthlem3  25354  ovolsslem  25385  ovolfiniun  25402  finiunmbl  25445  volfiniun  25448  iunmbl  25454  ioombl1lem4  25462  dyadmax  25499  vitali  25514  mbfimaopnlem  25556  mbflimsup  25567  mbfi1flim  25624  ditgeq3  25751  dvferm  25892  rollelem  25893  dvivthlem1  25913  itgsubstlem  25955  aalioulem2  26241  ulmcaulem  26303  ulmss  26306  xrlimcnp  26878  2sqreunnlem2  27366  pntlem3  27520  pntlemp  27521  pntleml  27522  nosepon  27577  noresle  27609  sssslt1  27707  sssslt2  27708  uspgr2wlkeq  29574  redwlk  29600  wwlksm1edg  29811  wwlksnred  29822  clwlkclwwlklem2  29929  clwwlkinwwlk  29969  clwwlkf  29976  wwlksubclwwlk  29987  occon  31216  xrge0infss  32683  resspos  32892  resstos  32893  gsummptres2  32993  submarchi  33140  prmidl2  33412  sigaclci  34122  measiun  34208  elmbfmvol2  34258  sibfof  34331  ftc2re  34589  bnj1118  34974  subfacp1lem3  35169  iccllysconn  35237  dmopab3rexdif  35392  untint  35699  untangtr  35701  dfon2lem6  35776  dfon2lem8  35778  dfon2lem9  35779  neibastop1  36347  neibastop2lem  36348  neibastop3  36350  weiunse  36456  finixpnum  37599  ptrecube  37614  poimirlem26  37640  poimirlem27  37641  poimirlem30  37644  heicant  37649  volsupnfl  37659  prdstotbnd  37788  heibor1lem  37803  ispridl2  38032  deg1gprod  42128  elrfirn2  42684  rabdiophlem1  42789  dford3lem1  43015  kelac1  43052  ssralv2  44521  ssralv2VD  44855  climinf  45604  limsupvaluz2  45736  supcnvlimsup  45738  iccpartres  47419  uhgrimisgrgric  47931  termc  49508