Theorem ssralv 4000

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 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		imim1 84	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1848	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)))
4		df-ral 3078	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
5		df-ral 3078	. . 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 2145  ∀wral 3077   ⊆ wss 3899

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 3078  df-ss 3916

This theorem is used by:  ss2ralv  4002  intss  4929  iinss1  4967  disjiun  5091  poss  5561  sess2  5617  isores3  7341  isoini2  7345  xpord2indlem  8157  xpord3inddlem  8164  poseq  8168  soseq  8169  smores  8353  smores2  8355  tfrlem5  8380  naddssim  8688  resixp  8954  ac6sfi  9268  iunfi  9325  ixpfi2  9332  marypha1lem  9418  ordtypelem2  9506  ttrclselem2  9720  tcrank  9894  acndom  10123  pwsdompw  10274  ssfin3ds  10401  fin1a2s  10485  hsmexlem4  10500  domtriomlem  10513  zornn0g  10576  fpwwe2lem12  10720  ingru  10893  cshw1  14966  rexanuz  15506  cau3lem  15515  caubnd  15519  limsupgord  15632  limsupval2  15640  rlimres  15718  lo1res  15719  o1of2  15773  o1rlimmul  15779  climsup  15830  fsumiun  15981  lcmfunsnlem1  16805  coprmprod  16829  pcfac  17070  vdwnnlem2  17167  firest  17596  imasaddfnlem  17693  imasvscafn  17702  resspos  18596  resstos  18597  psss  18747  tsrss  18756  idressidex0  18853  idressid  18855  cntz2ss  19542  cntzmhm2  19549  subgpgp  19804  efgsres  19945  telgsumfzs  20196  telgsums  20200  dprdss  20238  acsfn1p  21049  prmidl2  21615  ocv2ss  21972  mretopd  23403  tgcn  23563  tgcnp  23564  subbascn  23565  cnss2  23588  cncnp  23591  sslm  23610  t1ficld  23638  tgcmp  23712  1stcfb  23756  islly2  23796  dislly  23809  comppfsc  23844  ptbasfi  23893  ptcnplem  23933  tx1stc  23962  qtoptop2  24011  fbunfip  24181  flftg  24308  txflf  24318  fclsbas  24333  fclsss1  24334  fclsss2  24335  alexsubb  24358  tmdgsum2  24408  metrest  24836  rescncf  25211  cnllycmp  25270  bndth  25272  fgcfil  25585  ivthlem2  25766  ivthlem3  25767  ovolsslem  25798  ovolfiniun  25815  finiunmbl  25858  volfiniun  25861  iunmbl  25867  ioombl1lem4  25875  dyadmax  25912  vitali  25927  mbfimaopnlem  25969  mbflimsup  25980  mbfi1flim  26037  ditgeq3  26163  dvferm  26301  rollelem  26302  dvivthlem1  26321  itgsubstlem  26361  rnplynfin  26623  aalioulem2  26653  ulmcaulem  26714  ulmss  26717  xrlimcnp  27289  2sqreunnlem2  27775  pntlem3  27929  pntlemp  27930  pntleml  27931  nosepon  28015  noresle  28047  ssslts1  28152  ssslts2  28153  uspgr2wlkeq  30219  redwlk  30244  wwlksm1edg  30463  wwlksnred  30474  clwlkclwwlklem2  30584  clwwlkinwwlk  30624  clwwlkf  30631  wwlksubclwwlk  30642  occon  31882  xrge0infss  33345  gsummptres2  33607  submarchi  33740  sigaclci  34757  measiun  34844  elmbfmvol2  34892  sibfof  34965  ftc2re  35220  bnj1118  35607  subfacp1lem3  35926  iccllysconn  35994  dmopab3rexdif  36149  untint  36456  untangtr  36458  dfon2lem6  36530  dfon2lem8  36532  dfon2lem9  36533  neibastop1  37127  neibastop2lem  37128  neibastop3  37130  weiunse  37236  finixpnum  38508  ptrecube  38518  poimirlem26  38544  poimirlem27  38545  poimirlem30  38548  heicant  38553  volsupnfl  38563  prdstotbnd  38708  heibor1lem  38723  ispridl2  38952  deg1gprod  43170  elrfirn2  43686  rabdiophlem1  43787  dford3lem1  44012  kelac1  44049  ssralv2  45499  ssralv2VD  45833  climinf  46587  limsupvaluz2  46717  supcnvlimsup  46719  iccpartres  48469  uhgrimisgrgric  48998  termc  50596