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

Theorem r19.41v 2559
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 1489 . 2  |-  F/ x ps
21r19.41 2558 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   E.wrex 2389
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495
This theorem depends on definitions:  df-bi 116  df-nf 1418  df-rex 2394
This theorem is referenced by:  r19.42v  2560  3reeanv  2573  reuind  2856  iuncom4  3784  dfiun2g  3809  iunxiun  3858  inuni  4038  xpiundi  4555  xpiundir  4556  imaco  5000  coiun  5004  abrexco  5612  imaiun  5613  isoini  5671  rexrnmpo  5838  mapsnen  6657  genpassl  7274  genpassu  7275  4fvwrd4  9804  metrest  12489
  Copyright terms: Public domain W3C validator