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

Theorem albidv 1680
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
albidv.1
Assertion
Ref Expression
albidv
Distinct variable group:   ,

Proof of Theorem albidv
StepHypRef Expression
1 ax-5 1671 . 2
2 albidv.1 . 2
31, 2albidh 1643 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1368
This theorem is referenced by:  2albidv  1682  ax12wdemo  1770  ax12vALT  2137  sbcom2OLD  2158  axc11n-16  2245  eujust  2261  eujustALT  2262  euf  2269  eufOLD  2270  mo2  2271  moOLD  2311  axext3  2431  bm1.1  2433  bm1.1OLD  2434  eqeq1d  2452  eqeq1OLD  2454  nfceqdf  2605  ralbidv2  2810  ralxpxfr2d  3165  alexeqg  3169  alexeq  3170  pm13.183  3181  eqeu  3211  mo2icl  3219  euind  3227  reuind  3244  cdeqal  3257  sbcal  3320  sbcalgOLD  3321  sbcabel  3357  csbiebg  3393  ssconb  3571  reldisj  3804  sbcssg  3872  elint  4216  axrep1  4486  axrep2  4487  axrep3  4488  axrep4  4489  zfrepclf  4491  axsep2  4496  zfauscl  4497  bm1.3ii  4498  eusv1  4568  euotd  4674  freq1  4772  frsn  4991  iota5  5483  sbcfung  5523  funimass4  5825  dffo3  5941  eufnfv  6034  dff13  6054  tfisi  6553  dfom2  6562  elom  6563  seqomlem2  6990  pssnn  7616  findcard  7636  findcard2  7637  findcard3  7640  fiint  7673  inf0  7912  axinf2  7931  tz9.1  8034  karden  8187  aceq0  8373  dfac5  8383  zfac  8714  brdom3  8780  axpowndlem3  8849  axpowndlem3OLD  8850  zfcndrep  8866  zfcndac  8871  elgch  8874  engch  8880  axgroth3  9083  axgroth4  9084  elnp  9241  elnpi  9242  infm3  10374  fz1sbc  11621  uzrdgfni  11866  vdwmc2  14126  ramtlecl  14147  ramval  14155  ramub  14160  rami  14162  ramcl  14176  mreexexd  14672  mplsubglem  17601  mpllsslem  17602  mplsubglemOLD  17603  mpllsslemOLD  17604  istopg  18608  1stccn  19167  iskgen3  19222  fbfinnfr  19514  cnextfun  19736  metcld  20916  metcld2  20917  cusgrauvtxb  23523  isass  23922  chlimi  24756  nmcexi  25549  disjrdx  26051  funcnvmpt  26105  relexpindlem  27459  dfon2lem6  27719  dfon2lem7  27720  dfon2lem8  27721  dfon2  27723  sscoid  28062  wl-mo2t  28518  trer  28633  pm14.122b  29799  iotavalb  29806  trsbc  31528  bj-axext3  32570  bj-axrep1  32590  bj-axrep2  32591  bj-axrep3  32592  bj-axrep4  32593  bj-sbceqgALT  32685  bj-axsep2  32709  cdlemefrs29bpre0  34321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator