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

Theorem r19.21v 2547
Description: Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.21v  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem r19.21v
StepHypRef Expression
1 nfv 1521 . 2  |-  F/ x ph
21r19.21 2546 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wral 2448
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-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453
This theorem is referenced by:  r19.32vdc  2619  rmo4  2923  rmo3  3046  dftr5  4090  reusv3  4445  tfrlem1  6287  tfrlemi1  6311  tfr1onlemaccex  6327  tfrcllemaccex  6340  tfri3  6346  ordiso2  7012  raluz2  9538  ndvdssub  11889  nninfalllem1  14041  nninfsellemqall  14048
  Copyright terms: Public domain W3C validator