MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssralv Structured version   Visualization version   GIF version

Theorem ssralv 3699
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
StepHypRef Expression
1 ssel 3630 . . 3 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 82 . 2 (𝐴𝐵 → ((𝑥𝐵𝜑) → (𝑥𝐴𝜑)))
32ralimdv2 2990 1 (𝐴𝐵 → (∀𝑥𝐵 𝜑 → ∀𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wral 2941  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-in 3614  df-ss 3621
This theorem is referenced by:  intss  4530  iinss1  4565  disjiun  4672  poss  5066  sess2  5112  isores3  6625  isoini2  6629  smores  7494  smores2  7496  tfrlem5  7521  resixp  7985  ac6sfi  8245  iunfi  8295  ixpfi2  8305  dffi3  8378  marypha1lem  8380  ordtypelem2  8465  tcrank  8785  acndom  8912  pwsdompw  9064  ssfin3ds  9190  fin1a2s  9274  hsmexlem4  9289  domtriomlem  9302  zornn0g  9365  fpwwe2lem13  9502  ingru  9675  cshw1  13614  rexanuz  14129  cau3lem  14138  caubnd  14142  limsupgord  14247  limsupval2  14255  rlimres  14333  lo1res  14334  o1of2  14387  o1rlimmul  14393  isercolllem1  14439  climsup  14444  fsumiun  14597  lcmfunsnlem1  15397  coprmprod  15422  pcfac  15650  vdwnnlem2  15747  firest  16140  imasaddfnlem  16235  imasvscafn  16244  psss  17261  tsrss  17270  cntz2ss  17811  cntzmhm2  17818  subgpgp  18058  efgsres  18197  telgsumfzs  18432  telgsums  18436  dprdss  18474  ocv2ss  20065  mretopd  20944  tgcn  21104  tgcnp  21105  subbascn  21106  cnss2  21129  cncnp  21132  sslm  21151  t1ficld  21179  tgcmp  21252  1stcfb  21296  islly2  21335  dislly  21348  comppfsc  21383  ptbasfi  21432  ptcnplem  21472  tx1stc  21501  qtoptop2  21550  fbunfip  21720  flftg  21847  txflf  21857  fclsbas  21872  fclsss1  21873  fclsss2  21874  alexsubb  21897  tmdgsum2  21947  metrest  22376  rescncf  22747  cnllycmp  22802  bndth  22804  fgcfil  23115  cfilres  23140  ivthlem2  23267  ivthlem3  23268  ovolsslem  23298  ovolfiniun  23315  finiunmbl  23358  volfiniun  23361  iunmbl  23367  ioombl1lem4  23375  dyadmax  23412  vitali  23427  mbfimaopnlem  23467  mbflimsup  23478  mbfi1flim  23535  ditgeq3  23659  dvferm  23796  rollelem  23797  dvivthlem1  23816  itgsubstlem  23856  aalioulem2  24133  ulmcaulem  24193  ulmss  24196  xrlimcnp  24740  lgsdchr  25125  pntlem3  25343  pntlemp  25344  pntleml  25345  uspgr2wlkeq  26598  redwlk  26625  wwlksm1edg  26835  wwlksnred  26855  clwlkclwwlklem2  26966  clwwlkinwwlk  27003  clwwlkf  27010  wwlksubclwwlk  27023  occon  28274  xrge0infss  29653  resspos  29787  resstos  29788  submarchi  29868  sigaclci  30323  measiun  30409  elmbfmvol2  30457  sibfof  30530  ftc2re  30804  bnj1118  31178  subfacp1lem3  31290  iccllysconn  31358  untint  31715  untangtr  31717  dfon2lem6  31817  dfon2lem8  31819  dfon2lem9  31820  poseq  31878  soseq  31879  nosepon  31943  noresle  31971  sssslt1  32031  sssslt2  32032  neibastop1  32479  neibastop2lem  32480  neibastop3  32482  finixpnum  33524  ptrecube  33539  poimirlem26  33565  poimirlem27  33566  poimirlem30  33569  heicant  33574  volsupnfl  33584  prdstotbnd  33723  heibor1lem  33738  ispridl2  33967  elrfirn2  37576  rabdiophlem1  37682  dford3lem1  37910  kelac1  37950  acsfn1p  38086  ssralv2  39054  ssralv2VD  39416  climinf  40156  limsupvaluz2  40288  supcnvlimsup  40290  iccpartres  41679
  Copyright terms: Public domain W3C validator