Theorem ssralv 4032

Description: Quantification restricted to a subclass. (Contributed by NM, 11-Mar-2006.)

Assertion

Ref	Expression
ssralv	⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ssralv

Step	Hyp	Ref	Expression
1		ssel 3960	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 82	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)))
3	2	ralimdv2 3176	1 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3138   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-in 3942  df-ss 3951

This theorem is referenced by:  ss2ralv  4034  intss  4896  iinss1  4933  disjiun  5052  poss  5475  sess2  5523  isores3  7087  isoini2  7091  smores  7988  smores2  7990  tfrlem5  8015  resixp  8496  ac6sfi  8761  iunfi  8811  ixpfi2  8821  marypha1lem  8896  ordtypelem2  8982  tcrank  9312  acndom  9476  pwsdompw  9625  ssfin3ds  9751  fin1a2s  9835  hsmexlem4  9850  domtriomlem  9863  zornn0g  9926  fpwwe2lem13  10063  ingru  10236  cshw1  14183  rexanuz  14704  cau3lem  14713  caubnd  14717  limsupgord  14828  limsupval2  14836  rlimres  14914  lo1res  14915  o1of2  14968  o1rlimmul  14974  climsup  15025  fsumiun  15175  lcmfunsnlem1  15980  coprmprod  16004  pcfac  16234  vdwnnlem2  16331  firest  16705  imasaddfnlem  16800  imasvscafn  16809  psss  17823  tsrss  17832  cntz2ss  18462  cntzmhm2  18469  subgpgp  18721  efgsres  18863  telgsumfzs  19108  telgsums  19112  dprdss  19150  acsfn1p  19577  ocv2ss  20816  mretopd  21699  tgcn  21859  tgcnp  21860  subbascn  21861  cnss2  21884  cncnp  21887  sslm  21906  t1ficld  21934  tgcmp  22008  1stcfb  22052  islly2  22091  dislly  22104  comppfsc  22139  ptbasfi  22188  ptcnplem  22228  tx1stc  22257  qtoptop2  22306  fbunfip  22476  flftg  22603  txflf  22613  fclsbas  22628  fclsss1  22629  fclsss2  22630  alexsubb  22653  tmdgsum2  22703  metrest  23133  rescncf  23504  cnllycmp  23559  bndth  23561  fgcfil  23873  ivthlem2  24052  ivthlem3  24053  ovolsslem  24084  ovolfiniun  24101  finiunmbl  24144  volfiniun  24147  iunmbl  24153  ioombl1lem4  24161  dyadmax  24198  vitali  24213  mbfimaopnlem  24255  mbflimsup  24266  mbfi1flim  24323  ditgeq3  24447  dvferm  24584  rollelem  24585  dvivthlem1  24604  itgsubstlem  24644  aalioulem2  24921  ulmcaulem  24981  ulmss  24984  xrlimcnp  25545  2sqreunnlem2  26030  pntlem3  26184  pntlemp  26185  pntleml  26186  uspgr2wlkeq  27426  redwlk  27453  wwlksm1edg  27658  wwlksnred  27669  clwlkclwwlklem2  27777  clwwlkinwwlk  27817  clwwlkf  27825  wwlksubclwwlk  27836  occon  29063  xrge0infss  30483  resspos  30646  resstos  30647  submarchi  30815  prmidl2  30958  sigaclci  31391  measiun  31477  elmbfmvol2  31525  sibfof  31598  ftc2re  31869  bnj1118  32256  subfacp1lem3  32429  iccllysconn  32497  dmopab3rexdif  32652  untint  32938  untangtr  32940  dfon2lem6  33033  dfon2lem8  33035  dfon2lem9  33036  poseq  33095  soseq  33096  nosepon  33172  noresle  33200  sssslt1  33260  sssslt2  33261  neibastop1  33707  neibastop2lem  33708  neibastop3  33710  finixpnum  34876  ptrecube  34891  poimirlem26  34917  poimirlem27  34918  poimirlem30  34921  heicant  34926  volsupnfl  34936  prdstotbnd  35071  heibor1lem  35086  ispridl2  35315  elrfirn2  39291  rabdiophlem1  39396  dford3lem1  39621  kelac1  39661  ssralv2  40863  ssralv2VD  41198  climinf  41885  limsupvaluz2  42017  supcnvlimsup  42019  iccpartres  43577