Theorem ssralv 3982

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 3901	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2		imim1 84	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	al2imi 1848	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)))
4		df-ral 3081	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
5		df-ral 3081	. . 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 2147  ∀wral 3080   ⊆ wss 3900

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 3081  df-ss 3901

This theorem is used by:  ss2ralv  3984  intss  4932  iinss1  4970  disjiun  5094  poss  5566  sess2  5622  isores3  7372  isoini2  7376  xpord2indlem  8199  xpord3inddlem  8206  poseq  8210  soseq  8211  smores  8396  smores2  8398  tfrlem5  8423  naddssim  8731  resixp  8997  ac6sfi  9311  iunfi  9368  ixpfi2  9375  marypha1lem  9460  ordtypelem2  9548  ttrclselem2  9762  tcrank  9936  acndom  10167  pwsdompw  10318  ssfin3ds  10445  fin1a2s  10529  hsmexlem4  10544  domtriomlem  10557  zornn0g  10620  fpwwe2lem12  10764  ingru  10937  cshw1  15013  rexanuz  15554  cau3lem  15563  caubnd  15567  limsupgord  15680  limsupval2  15688  rlimres  15766  lo1res  15767  o1of2  15821  o1rlimmul  15827  climsup  15878  fsumiun  16029  lcmfunsnlem1  16853  coprmprod  16877  pcfac  17118  vdwnnlem2  17215  firest  17644  imasaddfnlem  17741  imasvscafn  17750  resspos  18644  resstos  18645  psss  18795  tsrss  18804  idressidex0  18901  idressid  18903  cntz2ss  19591  cntzmhm2  19598  subgpgp  19853  efgsres  19994  telgsumfzs  20245  telgsums  20249  dprdss  20287  acsfn1p  21098  prmidl2  21664  ocv2ss  22023  mretopd  23454  tgcn  23614  tgcnp  23615  subbascn  23616  cnss2  23639  cncnp  23642  sslm  23661  t1ficld  23689  tgcmp  23763  1stcfb  23807  islly2  23847  dislly  23860  comppfsc  23895  ptbasfi  23944  ptcnplem  23984  tx1stc  24013  qtoptop2  24062  fbunfip  24232  flftg  24359  txflf  24369  fclsbas  24384  fclsss1  24385  fclsss2  24386  alexsubb  24409  tmdgsum2  24459  metrest  24887  rescncf  25262  cnllycmp  25321  bndth  25323  fgcfil  25636  ivthlem2  25817  ivthlem3  25818  ovolsslem  25849  ovolfiniun  25866  finiunmbl  25909  volfiniun  25912  iunmbl  25918  ioombl1lem4  25926  dyadmax  25963  vitali  25978  mbfimaopnlem  26020  mbflimsup  26031  mbfi1flim  26088  ditgeq3  26214  dvferm  26352  rollelem  26353  dvivthlem1  26372  itgsubstlem  26412  rnplynfin  26674  aalioulem2  26706  ulmcaulem  26767  ulmss  26770  xrlimcnp  27342  2sqreunnlem2  27828  pntlem3  27982  pntlemp  27983  pntleml  27984  nosepon  28068  noresle  28100  ssslts1  28205  ssslts2  28206  uspgr2wlkeq  30272  redwlk  30297  wwlksm1edg  30516  wwlksnred  30527  clwlkclwwlklem2  30637  clwwlkinwwlk  30677  clwwlkf  30684  wwlksubclwwlk  30695  occon  31935  xrge0infss  33438  gsummptres2  33703  submarchi  33836  sigaclci  34868  measiun  34955  elmbfmvol2  35003  sibfof  35076  ftc2re  35331  bnj1118  35718  scottidm  35875  subfacp1lem3  36148  iccllysconn  36216  dmopab3rexdif  36371  untint  36685  untangtr  36687  dfon2lem6  36758  dfon2lem8  36760  dfon2lem9  36761  neibastop1  37355  neibastop2lem  37356  neibastop3  37358  weiunse  37464  finixpnum  38789  ptrecube  38799  poimirlem26  38825  poimirlem27  38826  poimirlem30  38829  heicant  38834  volsupnfl  38844  prdstotbnd  38987  heibor1lem  39002  ispridl2  39231  deg1gprod  43449  elrfirn2  43967  rabdiophlem1  44068  dford3lem1  44293  kelac1  44325  ssralv2  45768  ssralv2VD  46102  climinf  46885  limsupvaluz2  47015  supcnvlimsup  47017  iccpartres  48767  uhgrimisgrgric  49296  termc  50979