Theorem ssralv 3977

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 3896	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		imim1 84	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1847	. . 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 1567   ∈ wcel 2144  ∀wral 3076   ⊆ wss 3895

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

This proof depends on definitions:  df-bi 210  df-ral 3077  df-ss 3896

This theorem is used by:  ss2ralv  3979  intss  4928  iinss1  4966  disjiun  5090  poss  5560  sess2  5616  isores3  7344  isoini2  7348  xpord2indlem  8167  xpord3inddlem  8174  poseq  8178  soseq  8179  smores  8364  smores2  8366  tfrlem5  8391  naddssim  8699  resixp  8965  ac6sfi  9279  iunfi  9336  ixpfi2  9343  marypha1lem  9429  ordtypelem2  9517  ttrclselem2  9731  tcrank  9905  acndom  10134  pwsdompw  10285  ssfin3ds  10412  fin1a2s  10496  hsmexlem4  10511  domtriomlem  10524  zornn0g  10587  fpwwe2lem12  10731  ingru  10904  cshw1  14978  rexanuz  15519  cau3lem  15528  caubnd  15532  limsupgord  15645  limsupval2  15653  rlimres  15731  lo1res  15732  o1of2  15786  o1rlimmul  15792  climsup  15843  fsumiun  15994  lcmfunsnlem1  16818  coprmprod  16842  pcfac  17083  vdwnnlem2  17180  firest  17609  imasaddfnlem  17706  imasvscafn  17715  resspos  18609  resstos  18610  psss  18760  tsrss  18769  idressidex0  18866  idressid  18868  cntz2ss  19555  cntzmhm2  19562  subgpgp  19817  efgsres  19958  telgsumfzs  20209  telgsums  20213  dprdss  20251  acsfn1p  21062  prmidl2  21628  ocv2ss  21985  mretopd  23416  tgcn  23576  tgcnp  23577  subbascn  23578  cnss2  23601  cncnp  23604  sslm  23623  t1ficld  23651  tgcmp  23725  1stcfb  23769  islly2  23809  dislly  23822  comppfsc  23857  ptbasfi  23906  ptcnplem  23946  tx1stc  23975  qtoptop2  24024  fbunfip  24194  flftg  24321  txflf  24331  fclsbas  24346  fclsss1  24347  fclsss2  24348  alexsubb  24371  tmdgsum2  24421  metrest  24849  rescncf  25224  cnllycmp  25283  bndth  25285  fgcfil  25598  ivthlem2  25779  ivthlem3  25780  ovolsslem  25811  ovolfiniun  25828  finiunmbl  25871  volfiniun  25874  iunmbl  25880  ioombl1lem4  25888  dyadmax  25925  vitali  25940  mbfimaopnlem  25982  mbflimsup  25993  mbfi1flim  26050  ditgeq3  26176  dvferm  26314  rollelem  26315  dvivthlem1  26334  itgsubstlem  26374  rnplynfin  26636  aalioulem2  26666  ulmcaulem  26727  ulmss  26730  xrlimcnp  27302  2sqreunnlem2  27788  pntlem3  27942  pntlemp  27943  pntleml  27944  nosepon  28028  noresle  28060  ssslts1  28165  ssslts2  28166  uspgr2wlkeq  30232  redwlk  30257  wwlksm1edg  30476  wwlksnred  30487  clwlkclwwlklem2  30597  clwwlkinwwlk  30637  clwwlkf  30644  wwlksubclwwlk  30655  occon  31895  xrge0infss  33399  gsummptres2  33661  submarchi  33794  sigaclci  34811  measiun  34898  elmbfmvol2  34946  sibfof  35019  ftc2re  35274  bnj1118  35661  subfacp1lem3  36034  iccllysconn  36102  dmopab3rexdif  36257  untint  36570  untangtr  36572  dfon2lem6  36643  dfon2lem8  36645  dfon2lem9  36646  neibastop1  37240  neibastop2lem  37241  neibastop3  37243  weiunse  37349  finixpnum  38622  ptrecube  38632  poimirlem26  38658  poimirlem27  38659  poimirlem30  38662  heicant  38667  volsupnfl  38677  prdstotbnd  38822  heibor1lem  38837  ispridl2  39066  deg1gprod  43284  elrfirn2  43801  rabdiophlem1  43902  dford3lem1  44127  kelac1  44159  ssralv2  45608  ssralv2VD  45942  climinf  46712  limsupvaluz2  46842  supcnvlimsup  46844  iccpartres  48594  uhgrimisgrgric  49123  termc  50748