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

Theorem albidv 1632
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 1623 . 2  |-  ( ph  ->  A. x ph )
2 albidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2albidh 1597 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546
This theorem is referenced by:  2albidv  1634  ax11wdemo  1730  ax11vALT  2130  sbcom2  2147  ax10-16  2224  eujust  2240  eujustALT  2241  euf  2244  mo  2260  axext3  2370  bm1.1  2372  eqeq1  2393  nfceqdf  2522  ralbidv2  2671  alexeq  3008  pm13.183  3019  eqeu  3048  mo2icl  3056  euind  3064  reuind  3080  cdeqal  3093  sbcal  3151  sbcalg  3152  sbcabel  3181  csbiebg  3233  ssconb  3423  reldisj  3614  sbcss  3681  elint  3998  axrep1  4262  axrep2  4263  axrep3  4264  axrep4  4265  zfrepclf  4267  axsep2  4272  zfauscl  4273  bm1.3ii  4274  euotd  4398  freq1  4493  eusv1  4657  tfisi  4778  dfom2  4787  elom  4788  frsn  4888  iota5  5378  funimass4  5716  dffo3  5823  eufnfv  5911  dff13  5943  seqomlem2  6644  pssnn  7263  findcard  7283  findcard2  7284  findcard3  7286  fiint  7319  inf0  7509  axinf2  7528  tz9.1  7598  karden  7752  aceq0  7932  dfac5  7942  zfac  8273  brdom3  8339  axpowndlem3  8407  zfcndrep  8422  zfcndac  8427  elgch  8430  engch  8436  axgroth3  8639  axgroth4  8640  elnp  8797  elnpi  8798  infm3  9899  fz1sbc  11054  uzrdgfni  11225  vdwmc2  13274  ramtlecl  13295  ramval  13303  ramub  13308  rami  13310  ramcl  13324  mreexexd  13800  isclat  14465  oduclatb  14498  mplsubglem  16425  mpllsslem  16426  istopg  16891  1stccn  17447  iskgen3  17502  fbfinnfr  17794  cnextfun  18016  metcld  19129  metcld2  19130  nbusgra  21306  cusgrauvtxb  21371  isass  21752  chlimi  22585  nmcexi  23377  disjrdx  23874  funcnvmpt  23924  relexpindlem  24918  dfon2lem6  25168  dfon2lem7  25169  dfon2lem8  25170  dfon2  25172  elfuns  25478  trer  26010  ralxpxfr2d  26432  pm14.122b  27292  iotavalb  27299  sbcfun  27655  trsbc  27968  sbcom2OLD7  29077  cdlemefrs29bpre0  30510
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator