MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  raleqbi1dv Unicode version

Theorem raleqbi1dv 3062
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Hypothesis
Ref Expression
raleqd.1
Assertion
Ref Expression
raleqbi1dv
Distinct variable groups:   ,   ,

Proof of Theorem raleqbi1dv
StepHypRef Expression
1 raleq 3054 . 2
2 raleqd.1 . . 3
32ralbidv 2896 . 2
41, 3bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  A.wral 2807
This theorem is referenced by:  isoeq4  6218  smo11  7054  dffi2  7903  inficl  7905  dffi3  7911  dfom3  8085  aceq1  8519  dfac5lem4  8528  kmlem1  8551  kmlem10  8560  kmlem13  8563  kmlem14  8564  cofsmo  8670  infpssrlem4  8707  axdc3lem2  8852  elwina  9085  elina  9086  iswun  9103  eltskg  9149  elgrug  9191  elnp  9386  elnpi  9387  dfnn2  10574  dfnn3  10575  dfuzi  10978  ismri  15028  isprs  15559  isdrs  15563  ispos  15576  istos  15665  pospropd  15764  isipodrs  15791  isdlat  15823  mhmpropd  15972  issubm  15978  subgacs  16236  nsgacs  16237  isghm  16267  ghmeql  16289  iscmn  16805  dfrhm2  17366  islss  17581  lssacs  17613  lmhmeql  17701  islbs  17722  lbsextlem1  17804  lbsextlem3  17806  lbsextlem4  17807  isobs  18751  mat0dimcrng  18972  istopg  19404  isbasisg  19448  basis2  19452  eltg2  19459  iscldtop  19596  neipeltop  19630  isreg  19833  regsep  19835  isnrm  19836  islly  19969  isnlly  19970  llyi  19975  nllyi  19976  islly2  19985  cldllycmp  19996  isfbas  20330  fbssfi  20338  isust  20706  elutop  20736  ustuqtop  20749  utopsnneip  20751  ispsmet  20808  ismet  20826  isxmet  20827  metrest  21027  cncfval  21392  fmcfil  21711  iscfil3  21712  caucfil  21722  iscmet3  21732  cfilres  21735  minveclem3  21844  wilthlem2  23343  wilthlem3  23344  wilth  23345  isfrgra  24990  isplig  25179  isgrpo  25198  isablo  25285  ismndo2  25347  rngomndo  25423  disjabrex  27443  disjabrexf  27444  isomnd  27691  isorng  27789  isrnsigaOLD  28112  isrnsiga  28113  kur14lem9  28658  cvmscbv  28703  cvmsi  28710  cvmsval  28711  wfrlem1  29343  wfrlem4  29346  wfrlem15  29357  frrlem1  29387  frrlem4  29390  neibastop1  30177  neibastop2lem  30178  neibastop2  30179  isbnd  30276  isidl  30411  isnacs  30636  mzpclval  30657  elmzpcl  30658  mgmhmpropd  32473  issubmgm  32477  rnghmval  32697  zrrnghm  32723  bnj1286  34075  bnj1452  34108  ispsubsp  35469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812
  Copyright terms: Public domain W3C validator