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

Theorem albidv 1635
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 1626 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2albidh 1600 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549
This theorem is referenced by:  2albidv  1637  ax11wdemo  1738  ax11vALT  2172  sbcom2  2189  ax10-16  2266  eujust  2282  eujustALT  2283  euf  2286  mo  2302  axext3  2418  bm1.1  2420  eqeq1  2441  nfceqdf  2570  ralbidv2  2719  alexeq  3057  pm13.183  3068  eqeu  3097  mo2icl  3105  euind  3113  reuind  3129  cdeqal  3142  sbcal  3200  sbcalg  3201  sbcabel  3230  csbiebg  3282  ssconb  3472  reldisj  3663  sbcss  3730  elint  4048  axrep1  4313  axrep2  4314  axrep3  4315  axrep4  4316  zfrepclf  4318  axsep2  4323  zfauscl  4324  bm1.3ii  4325  euotd  4449  freq1  4544  eusv1  4709  tfisi  4830  dfom2  4839  elom  4840  frsn  4940  iota5  5430  funimass4  5769  dffo3  5876  eufnfv  5964  dff13  5996  seqomlem2  6700  pssnn  7319  findcard  7339  findcard2  7340  findcard3  7342  fiint  7375  inf0  7568  axinf2  7587  tz9.1  7657  karden  7811  aceq0  7991  dfac5  8001  zfac  8332  brdom3  8398  axpowndlem3  8466  zfcndrep  8481  zfcndac  8486  elgch  8489  engch  8495  axgroth3  8698  axgroth4  8699  elnp  8856  elnpi  8857  infm3  9959  fz1sbc  11116  uzrdgfni  11290  vdwmc2  13339  ramtlecl  13360  ramval  13368  ramub  13373  rami  13375  ramcl  13389  mreexexd  13865  isclat  14530  oduclatb  14563  mplsubglem  16490  mpllsslem  16491  istopg  16960  1stccn  17518  iskgen3  17573  fbfinnfr  17865  cnextfun  18087  metcld  19250  metcld2  19251  cusgrauvtxb  21497  isass  21896  chlimi  22729  nmcexi  23521  disjrdx  24023  funcnvmpt  24075  relexpindlem  25131  dfon2lem6  25407  dfon2lem7  25408  dfon2lem8  25409  dfon2  25411  sscoid  25750  trer  26300  ralxpxfr2d  26722  pm14.122b  27581  iotavalb  27588  sbcfun  27944  trsbc  28552  sbcom2NEW7  29571  cdlemefrs29bpre0  31120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator