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 3077	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
5		df-ral 3077	. . 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 3076   ⊆ 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 3077  df-ss 3916

This theorem is used by:  ss2ralv  4002  intss  4929  iinss1  4967  disjiun  5091  poss  5565  sess2  5621  isores3  7336  isoini2  7340  xpord2indlem  8145  xpord3inddlem  8152  poseq  8156  soseq  8157  smores  8341  smores2  8343  tfrlem5  8368  naddssim  8674  resixp  8940  ac6sfi  9254  iunfi  9310  ixpfi2  9317  marypha1lem  9403  ordtypelem2  9491  ttrclselem2  9705  tcrank  9866  acndom  10054  pwsdompw  10205  ssfin3ds  10332  fin1a2s  10416  hsmexlem4  10431  domtriomlem  10444  zornn0g  10507  fpwwe2lem12  10651  ingru  10824  cshw1  14893  rexanuz  15433  cau3lem  15442  caubnd  15446  limsupgord  15559  limsupval2  15567  rlimres  15645  lo1res  15646  o1of2  15700  o1rlimmul  15706  climsup  15757  fsumiun  15908  lcmfunsnlem1  16727  coprmprod  16751  pcfac  16991  vdwnnlem2  17088  firest  17517  imasaddfnlem  17614  imasvscafn  17623  resspos  18517  resstos  18518  psss  18668  tsrss  18677  idressidex0  18773  idressid  18775  cntz2ss  19462  cntzmhm2  19469  subgpgp  19724  efgsres  19865  telgsumfzs  20116  telgsums  20120  dprdss  20158  acsfn1p  20965  prmidl2  21529  ocv2ss  21886  mretopd  23317  tgcn  23477  tgcnp  23478  subbascn  23479  cnss2  23502  cncnp  23505  sslm  23524  t1ficld  23552  tgcmp  23626  1stcfb  23670  islly2  23710  dislly  23723  comppfsc  23758  ptbasfi  23807  ptcnplem  23847  tx1stc  23876  qtoptop2  23925  fbunfip  24095  flftg  24222  txflf  24232  fclsbas  24247  fclsss1  24248  fclsss2  24249  alexsubb  24272  tmdgsum2  24322  metrest  24750  rescncf  25125  cnllycmp  25184  bndth  25186  fgcfil  25499  ivthlem2  25680  ivthlem3  25681  ovolsslem  25712  ovolfiniun  25729  finiunmbl  25772  volfiniun  25775  iunmbl  25781  ioombl1lem4  25789  dyadmax  25826  vitali  25841  mbfimaopnlem  25883  mbflimsup  25894  mbfi1flim  25951  ditgeq3  26077  dvferm  26215  rollelem  26216  dvivthlem1  26235  itgsubstlem  26275  rnplynfin  26539  aalioulem2  26569  ulmcaulem  26630  ulmss  26633  xrlimcnp  27205  2sqreunnlem2  27691  pntlem3  27845  pntlemp  27846  pntleml  27847  nosepon  27901  noresle  27933  ssslts1  28038  ssslts2  28039  uspgr2wlkeq  30105  redwlk  30130  wwlksm1edg  30349  wwlksnred  30360  clwlkclwwlklem2  30470  clwwlkinwwlk  30510  clwwlkf  30517  wwlksubclwwlk  30528  occon  31768  xrge0infss  33231  gsummptres2  33493  submarchi  33626  sigaclci  34642  measiun  34729  elmbfmvol2  34778  sibfof  34851  ftc2re  35106  bnj1118  35493  subfacp1lem3  35761  iccllysconn  35829  dmopab3rexdif  35984  untint  36291  untangtr  36293  dfon2lem6  36365  dfon2lem8  36367  dfon2lem9  36368  neibastop1  36978  neibastop2lem  36979  neibastop3  36981  weiunse  37087  finixpnum  38359  ptrecube  38369  poimirlem26  38395  poimirlem27  38396  poimirlem30  38399  heicant  38404  volsupnfl  38414  prdstotbnd  38544  heibor1lem  38559  ispridl2  38788  deg1gprod  43006  elrfirn2  43541  rabdiophlem1  43642  dford3lem1  43867  kelac1  43904  ssralv2  45354  ssralv2VD  45688  climinf  46436  limsupvaluz2  46566  supcnvlimsup  46568  iccpartres  48318  uhgrimisgrgric  48847  termc  50445