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  2785  euind  2924  reuind  2942  snssb  3725  unissb  3839  disjnim  3994  dftr2  4103  ssrelrel  4726  cotr  5010  dffun2  5226  fununi  5284  dff13  5768  acexmidlem2  5871
  Copyright terms: Public domain W3C validator