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

Theorem r19.41v 2564
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 1493 . 2  |-  F/ x ps
21r19.41 2563 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 2394
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-rex 2399
This theorem is referenced by:  r19.42v  2565  3reeanv  2578  reuind  2862  iuncom4  3790  dfiun2g  3815  iunxiun  3864  inuni  4050  xpiundi  4567  xpiundir  4568  imaco  5014  coiun  5018  abrexco  5628  imaiun  5629  isoini  5687  rexrnmpo  5854  mapsnen  6673  genpassl  7300  genpassu  7301  4fvwrd4  9885  metrest  12602
  Copyright terms: Public domain W3C validator