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

Theorem albidv 1615
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
albidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
albidv  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem albidv
StepHypRef Expression
1 ax-17 1606 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2albidh 1580 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530
This theorem is referenced by:  2albidv  1617  ax11wdemo  1709  sbcom2  2066  ax10-16  2142  eujust  2158  eujustALT  2159  euf  2162  mo  2178  axext3  2279  bm1.1  2281  eqeq1  2302  nfceqdf  2431  ralbidv2  2578  alexeq  2910  pm13.183  2921  eqeu  2949  mo2icl  2957  euind  2965  reuind  2981  cdeqal  2993  sbcal  3051  sbcalg  3052  sbcabel  3081  csbiebg  3133  ssconb  3322  reldisj  3511  sbcss  3577  elint  3884  axrep1  4148  axrep2  4149  axrep3  4150  axrep4  4151  zfrepclf  4153  axsep2  4158  zfauscl  4159  bm1.3ii  4160  euotd  4283  freq1  4379  eusv1  4544  tfisi  4665  dfom2  4674  elom  4675  frsn  4776  iota5  5255  funimass4  5589  dffo3  5691  eufnfv  5768  dff13  5799  seqomlem2  6479  pssnn  7097  findcard  7113  findcard2  7114  findcard3  7116  fiint  7149  inf0  7338  axinf2  7357  tz9.1  7427  karden  7581  aceq0  7761  dfac5  7771  zfac  8102  brdom3  8169  axpowndlem3  8237  zfcndrep  8252  zfcndac  8257  elgch  8260  engch  8266  axgroth3  8469  axgroth4  8470  elnp  8627  elnpi  8628  infm3  9729  fz1sbc  10875  uzrdgfni  11037  vdwmc2  13042  ramtlecl  13063  ramval  13071  ramub  13076  rami  13078  ramcl  13092  mreexexd  13566  isclat  14231  oduclatb  14264  mplsubglem  16195  mpllsslem  16196  istopg  16657  1stccn  17205  iskgen3  17260  fbfinnfr  17552  metcld  18747  metcld2  18748  isass  20999  chlimi  21830  nmcexi  22622  disjrdx  23385  relexpindlem  24051  dfon2lem6  24215  dfon2lem7  24216  dfon2lem8  24217  dfon2  24219  elfuns  24525  alexeqd  25065  elintabg  25193  sgplpte21a  26236  trer  26330  ralxpxfr2d  26863  pm14.122b  27726  iotavalb  27733  sbcfun  28090  nbusgra  28277  trsbc  28603  sbcom2OLD7  29715  cdlemefrs29bpre0  31207
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator