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

Theorem r19.42v 2627
Description: Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
Assertion
Ref Expression
r19.42v  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem r19.42v
StepHypRef Expression
1 r19.41v 2626 . 2  |-  ( E. x  e.  A  ( ps  /\  ph )  <->  ( E. x  e.  A  ps  /\  ph ) )
2 ancom 264 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
32rexbii 2477 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
4 ancom 264 . 2  |-  ( (
ph  /\  E. x  e.  A  ps )  <->  ( E. x  e.  A  ps  /\  ph ) )
51, 3, 43bitr4i 211 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  (
ph  /\  E. x  e.  A  ps )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   E.wrex 2449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-rex 2454
This theorem is referenced by:  ceqsrexbv  2861  ceqsrex2v  2862  2reuswapdc  2934  iunrab  3920  iunin2  3936  iundif2ss  3938  iunopab  4266  elxp2  4629  cnvuni  4797  elunirn  5745  f1oiso  5805  oprabrexex2  6109  genpdflem  7469  1idprl  7552  1idpru  7553  ltexprlemm  7562  rexuz2  9540  4fvwrd4  10096  divalgb  11884
  Copyright terms: Public domain W3C validator