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

Theorem r19.21v 2605
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 1629 . 2  |-  F/ x ph
21r19.21 2604 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 2518
This theorem is referenced by:  r19.32v  2661  rmo4  2933  2reu5lem3  2947  rmo3  3053  dftr5  4090  reusv3  4514  tfinds2  4626  tfinds3  4627  tfr3  6383  oeordi  6553  ordiso2  7198  ordtypelem7  7207  cantnf  7363  dfac12lem3  7739  ttukeylem5  8108  ttukeylem6  8109  fpwwe2lem8  8227  grudomon  8407  raluz2  10235  ndvdssub  12568  gcdcllem1  12652  acsfn2  13527  pgpfac1  15277  pgpfac  15281  isdomn2  16002  isclo2  16787  1stccn  17151  kgencn  17213  txflf  17663  fclsopn  17671  rdgprc  23520  wfr3g  23624  bpolycl  24162  filnetlem4  25697  islindf4  26675  bnj580  27994  bnj852  28002
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-ral 2523
  Copyright terms: Public domain W3C validator