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

Theorem r19.41v 2511
Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 17-Dec-2003.)
Assertion
Ref Expression
r19.41v  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem r19.41v
StepHypRef Expression
1 nfv 1462 . 2  |-  F/ x ps
21r19.41 2510 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103   E.wrex 2350
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  df-nf 1391  df-rex 2355
This theorem is referenced by:  r19.42v  2512  3reeanv  2525  reuind  2796  iuncom4  3693  dfiun2g  3718  iunxiun  3765  inuni  3938  xpiundi  4424  xpiundir  4425  imaco  4856  coiun  4860  abrexco  5430  imaiun  5431  isoini  5488  rexrnmpt2  5647  genpassl  6776  genpassu  6777  4fvwrd4  9227
  Copyright terms: Public domain W3C validator