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

Theorem r19.21v 2534
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 1508 . 2  |-  F/ x ph
21r19.21 2533 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 2435
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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ial 1514  ax-i5r 1515
This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440
This theorem is referenced by:  r19.32vdc  2606  rmo4  2905  rmo3  3028  dftr5  4065  reusv3  4420  tfrlem1  6255  tfrlemi1  6279  tfr1onlemaccex  6295  tfrcllemaccex  6308  tfri3  6314  ordiso2  6979  raluz2  9490  ndvdssub  11821  nninfalllem1  13591  nninfsellemqall  13598
  Copyright terms: Public domain W3C validator