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

Theorem 19.42v 1828
Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.42v  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem 19.42v
StepHypRef Expression
1 ax-17 1460 . 2  |-  ( ph  ->  A. x ph )
2119.42h 1618 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  exdistr  1829  19.42vv  1830  19.42vvv  1831  4exdistr  1835  cbvex2  1839  2sb5  1901  2sb5rf  1907  rexcom4a  2624  ceqsex2  2640  reuind  2796  2rmorex  2797  sbccomlem  2889  bm1.3ii  3907  opm  3997  eqvinop  4006  uniuni  4209  dmopabss  4575  dmopab3  4576  mptpreima  4844  brprcneu  5202  relelfvdm  5237  fndmin  5306  fliftf  5470  dfoprab2  5583  dmoprab  5616  dmoprabss  5617  fnoprabg  5633  opabex3d  5779  opabex3  5780  eroveu  6263  dmaddpq  6631  dmmulpq  6632  prarloc  6755  ltexprlemopl  6853  ltexprlemlol  6854  ltexprlemopu  6855  ltexprlemupu  6856  shftdm  9848  bdbm1.3ii  10840
  Copyright terms: Public domain W3C validator