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

Theorem albidv 1713
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 1704 . 2
2 albidv.1 . 2
31, 2albidh 1675 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393
This theorem is referenced by:  2albidv  1715  ax12wdemo  1831  ax12vOLD  1856  axc11n-16  2268  eujust  2284  eujustALT  2285  euf  2292  mo2  2293  axext3  2437  axext3OLD  2438  bm1.1  2440  bm1.1OLD  2441  eqeq1dALT  2460  eqeq1OLD  2462  nfceqdf  2614  ralbidv2  2892  ralxpxfr2d  3224  alexeqg  3228  alexeq  3229  pm13.183  3240  eqeu  3270  mo2icl  3278  euind  3286  reuind  3303  cdeqal  3316  sbcal  3379  sbcalgOLD  3380  sbcabel  3416  csbiebg  3457  ssconb  3636  reldisj  3870  sbcssg  3940  elint  4292  axrep1  4564  axrep2  4565  axrep3  4566  axrep4  4567  zfrepclf  4569  axsep2  4574  zfauscl  4575  bm1.3ii  4576  eusv1  4646  euotd  4753  freq1  4854  frsn  5075  iota5  5576  sbcfung  5616  funimass4  5924  dffo3  6046  eufnfv  6146  dff13  6166  tfisi  6693  dfom2  6702  elom  6703  seqomlem2  7135  pssnn  7758  findcard  7779  findcard2  7780  findcard3  7783  fiint  7817  inf0  8059  axinf2  8078  tz9.1  8181  karden  8334  aceq0  8520  dfac5  8530  zfac  8861  brdom3  8927  axpowndlem3  8996  axpowndlem3OLD  8997  zfcndrep  9013  zfcndac  9018  elgch  9021  engch  9027  axgroth3  9230  axgroth4  9231  elnp  9386  elnpi  9387  infm3  10527  fz1sbc  11783  uzrdgfni  12069  vdwmc2  14497  ramtlecl  14518  ramval  14526  ramub  14531  rami  14533  ramcl  14547  mreexexd  15045  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  istopg  19404  1stccn  19964  iskgen3  20050  fbfinnfr  20342  cnextfun  20564  metcld  21744  metcld2  21745  cusgrauvtxb  24496  isass  25318  chlimi  26152  nmcexi  26945  disjrdx  27450  funcnvmpt  27510  mclsssvlem  28922  mclsval  28923  mclsind  28930  relexpindlem  29062  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon2  29224  sscoid  29563  wl-mo2t  30020  trer  30134  pm14.122b  31330  iotavalb  31337  trsbc  33311  bj-axext3  34354  bj-axrep1  34374  bj-axrep2  34375  bj-axrep3  34376  bj-axrep4  34377  bj-sbceqgALT  34469  bj-axsep2  34493  bj-nuliota  34586  cdlemefrs29bpre0  36122
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
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator