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

Theorem albid 1789
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 1779 . 2  |-  ( ph  ->  A. x ph )
3 albid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3albidh 1601 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550   F/wnf 1554
This theorem is referenced by:  nfbidf  1791  dral2  2056  ax11v2  2079  ax11v2OLD  2080  sbcom  2166  sbcomOLD  2167  sbal2  2213  ax11eq  2272  ax11el  2273  ax11v2-o  2280  eubid  2290  ralbida  2721  raleqf  2902  intab  4082  fin23lem32  8229  axrepndlem1  8472  axrepndlem2  8473  axrepnd  8474  axunnd  8476  axpowndlem2  8478  axpowndlem4  8480  axregndlem2  8483  axinfndlem1  8485  axinfnd  8486  axacndlem4  8490  axacndlem5  8491  axacnd  8492  funcnvmptOLD  24087  iota5f  25187  dral2w3AUX7  29576  ax11v2NEW7  29604  sbcomwAUX7  29662  ax7w15lemAUX7  29741  ax7w14lemAUX7  29743  sbcomOLD7  29829  sbal2OLD7  29842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator