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

Theorem r19.41v 2646
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 1539 . 2  |-  F/ x ps
21r19.41 2645 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105   E.wrex 2469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-rex 2474
This theorem is referenced by:  r19.42v  2647  3reeanv  2661  reuind  2957  iuncom4  3908  dfiun2g  3933  iunxiun  3983  inuni  4173  xpiundi  4702  xpiundir  4703  imaco  5152  coiun  5156  abrexco  5781  imaiun  5782  isoini  5840  rexrnmpo  6012  mapsnen  6837  genpassl  7553  genpassu  7554  4fvwrd4  10170  4sqlem12  12434  metrest  14463  trirec0xor  15252
  Copyright terms: Public domain W3C validator