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

Theorem r19.21v 2808
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 1673 . 2  |-  F/ x ph
21r19.21 2807 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wral 2720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590  df-ral 2725
This theorem is referenced by:  r19.32v  2871  rmo4  3157  2reu5lem3  3171  rmo3  3290  dftr5  4393  reusv3  4505  tfinds2  6479  tfinds3  6480  tfrlem1  6840  tfr3  6863  oeordi  7031  ordiso2  7734  ordtypelem7  7743  cantnf  7906  cantnfOLD  7928  dfac12lem3  8319  ttukeylem5  8687  ttukeylem6  8688  fpwwe2lem8  8809  grudomon  8989  raluz2  10909  ndvdssub  13616  gcdcllem1  13700  acsfn2  14606  pgpfac1  16586  pgpfac  16590  isdomn2  17376  islindf4  18272  isclo2  18697  1stccn  19072  kgencn  19134  txflf  19584  fclsopn  19592  nn0min  26095  rdgprc  27613  wfr3g  27728  bpolycl  28200  heicant  28431  filnetlem4  28607  2rexrsb  30000  bnj580  31911  bnj852  31919
  Copyright terms: Public domain W3C validator