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

Theorem r19.21v 2583
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 1551 . 2  |-  F/ x ph
21r19.21 2582 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   A.wral 2484
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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558
This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489
This theorem is referenced by:  r19.32vdc  2655  rmo4  2966  rmo3  3090  dftr5  4146  reusv3  4508  tfrlem1  6396  tfrlemi1  6420  tfr1onlemaccex  6436  tfrcllemaccex  6449  tfri3  6455  ordiso2  7139  raluz2  9702  ndvdssub  12274  nninfalllem1  15982  nninfsellemqall  15989
  Copyright terms: Public domain W3C validator