MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.21v Unicode version

Theorem r19.21v 2630
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 1605 . 2  |-  F/ x ph
21r19.21 2629 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2543
This theorem is referenced by:  r19.32v  2686  rmo4  2958  2reu5lem3  2972  rmo3  3078  dftr5  4116  reusv3  4542  tfinds2  4654  tfinds3  4655  tfr3  6415  oeordi  6585  ordiso2  7230  ordtypelem7  7239  cantnf  7395  dfac12lem3  7771  ttukeylem5  8140  ttukeylem6  8141  fpwwe2lem8  8259  grudomon  8439  raluz2  10268  ndvdssub  12606  gcdcllem1  12690  acsfn2  13565  pgpfac1  15315  pgpfac  15319  isdomn2  16040  isclo2  16825  1stccn  17189  kgencn  17251  txflf  17701  fclsopn  17709  rdgprc  24151  wfr3g  24255  bpolycl  24787  filnetlem4  26330  islindf4  27308  2rexrsb  27949  bnj580  28945  bnj852  28953
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator