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

Theorem albidv 1611
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 1603 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2albidh 1577 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527
This theorem is referenced by:  2albidv  1613  ax11wdemo  1697  sbcom2  2053  ax10-16  2129  eujust  2145  eujustALT  2146  euf  2149  mo  2165  axext3  2266  bm1.1  2268  eqeq1  2289  nfceqdf  2418  ralbidv2  2565  alexeq  2897  pm13.183  2908  eqeu  2936  mo2icl  2944  euind  2952  reuind  2968  cdeqal  2980  sbcal  3038  sbcalg  3039  sbcabel  3068  csbiebg  3120  ssconb  3309  reldisj  3498  sbcss  3564  elint  3868  axrep1  4132  axrep2  4133  axrep3  4134  axrep4  4135  zfrepclf  4137  axsep2  4142  zfauscl  4143  bm1.3ii  4144  euotd  4267  freq1  4363  eusv1  4528  tfisi  4649  dfom2  4658  elom  4659  frsn  4760  iota5  5239  funimass4  5573  dffo3  5675  eufnfv  5752  dff13  5783  seqomlem2  6463  pssnn  7081  findcard  7097  findcard2  7098  findcard3  7100  fiint  7133  inf0  7322  axinf2  7341  tz9.1  7411  karden  7565  aceq0  7745  dfac5  7755  zfac  8086  brdom3  8153  axpowndlem3  8221  zfcndrep  8236  zfcndac  8241  elgch  8244  engch  8250  axgroth3  8453  axgroth4  8454  elnp  8611  elnpi  8612  infm3  9713  fz1sbc  10859  uzrdgfni  11021  vdwmc2  13026  ramtlecl  13047  ramval  13055  ramub  13060  rami  13062  ramcl  13076  mreexexd  13550  isclat  14215  oduclatb  14248  mplsubglem  16179  mpllsslem  16180  istopg  16641  1stccn  17189  iskgen3  17244  fbfinnfr  17536  metcld  18731  metcld2  18732  isass  20983  chlimi  21814  nmcexi  22606  disjrdx  23370  relexpindlem  24036  dfon2lem6  24144  dfon2lem7  24145  dfon2lem8  24146  dfon2  24148  elfuns  24454  alexeqd  24962  elintabg  25090  sgplpte21a  26133  trer  26227  ralxpxfr2d  26760  pm14.122b  27623  iotavalb  27630  sbcfun  27985  nbusgra  28143  trsbc  28304  cdlemefrs29bpre0  30585
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator