ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  19.23v Unicode version

Theorem 19.23v 1883
Description: Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
Assertion
Ref Expression
19.23v  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem 19.23v
StepHypRef Expression
1 ax-17 1526 . 2  |-  ( ps 
->  A. x ps )
2119.23h 1498 1  |-  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   A.wal 1351   E.wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-gen 1449  ax-ie2 1494  ax-17 1526
This theorem is referenced by:  19.23vv  1884  2eu4  2119  gencbval  2787  euind  2926  reuind  2944  snssb  3727  unissb  3841  disjnim  3996  dftr2  4105  ssrelrel  4728  cotr  5012  dffun2  5228  fununi  5286  dff13  5771  acexmidlem2  5874
  Copyright terms: Public domain W3C validator