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

Theorem albid 1764
Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
albid.1  |-  F/ x ph
albid.2  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
albid  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )

Proof of Theorem albid
StepHypRef Expression
1 albid.1 . . 3  |-  F/ x ph
21nfri 1754 . 2  |-  ( ph  ->  A. x ph )
3 albid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3albidh 1580 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530   F/wnf 1534
This theorem is referenced by:  nfbidf  1766  ax11v2  1945  sbcom  2042  sbal2  2086  ax11eq  2145  ax11el  2146  ax11v2-o  2153  eubid  2163  ralbida  2570  raleqf  2745  intab  3908  fin23lem32  7986  axrepndlem1  8230  axrepndlem2  8231  axrepnd  8232  axunnd  8234  axpowndlem2  8236  axpowndlem4  8238  axregndlem2  8241  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250  funcnvmptOLD  23249  funcnvmpt  23250  dral2w3AUX7  29479  ax11v2NEW7  29505  sbcomwAUX7  29562  sbcomOLD7  29709  sbal2OLD7  29724
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  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator