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

Theorem albid 1788
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 1778 . 2  |-  ( ph  ->  A. x ph )
3 albid.2 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3albidh 1600 1  |-  ( ph  ->  ( A. x ps  <->  A. x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549   F/wnf 1553
This theorem is referenced by:  nfbidf  1790  dral2  2051  ax11v2  2074  ax11v2OLD  2075  sbcom  2164  sbcomOLD  2165  sbal2  2211  ax11eq  2270  ax11el  2271  ax11v2-o  2278  eubid  2288  ralbida  2712  raleqf  2893  intab  4073  fin23lem32  8217  axrepndlem1  8460  axrepndlem2  8461  axrepnd  8462  axunnd  8464  axpowndlem2  8466  axpowndlem4  8468  axregndlem2  8471  axinfndlem1  8473  axinfnd  8474  axacndlem4  8478  axacndlem5  8479  axacnd  8480  funcnvmptOLD  24075  iota5f  25175  dral2w3AUX7  29440  ax11v2NEW7  29468  sbcomwAUX7  29526  ax7w15lemAUX7  29605  ax7w14lemAUX7  29607  sbcomOLD7  29693  sbal2OLD7  29706
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  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator