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

Theorem r19.21v 2631
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 1606 . 2  |-  F/ x ph
21r19.21 2630 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   A.wral 2544
This theorem is referenced by:  r19.32v  2687  rmo4  2959  2reu5lem3  2973  rmo3  3079  dftr5  4117  reusv3  4541  tfinds2  4653  tfinds3  4654  tfr3  6410  oeordi  6580  ordiso2  7225  ordtypelem7  7234  cantnf  7390  dfac12lem3  7766  ttukeylem5  8135  ttukeylem6  8136  fpwwe2lem8  8254  grudomon  8434  raluz2  10263  ndvdssub  12600  gcdcllem1  12684  acsfn2  13559  pgpfac1  15309  pgpfac  15313  isdomn2  16034  isclo2  16819  1stccn  17183  kgencn  17245  txflf  17695  fclsopn  17703  rdgprc  23552  wfr3g  23656  bpolycl  24194  filnetlem4  25729  islindf4  26707  2rexrsb  27328  bnj580  28212  bnj852  28220
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1533  df-ral 2549
  Copyright terms: Public domain W3C validator