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

Theorem r19.21v 2793
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 1672 . 2  |-  F/ x ph
21r19.21 2792 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 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-nf 1593  df-ral 2710
This theorem is referenced by:  r19.32v  2856  rmo4  3141  2reu5lem3  3155  rmo3  3273  dftr5  4376  reusv3  4488  tfinds2  6463  tfinds3  6464  tfrlem1  6821  tfr3  6844  oeordi  7014  ordiso2  7717  ordtypelem7  7726  cantnf  7889  cantnfOLD  7911  dfac12lem3  8302  ttukeylem5  8670  ttukeylem6  8671  fpwwe2lem8  8791  grudomon  8971  raluz2  10891  ndvdssub  13593  gcdcllem1  13677  acsfn2  14583  pgpfac1  16554  pgpfac  16558  isdomn2  17292  islindf4  18108  isclo2  18533  1stccn  18908  kgencn  18970  txflf  19420  fclsopn  19428  nn0min  25912  rdgprc  27454  wfr3g  27569  bpolycl  28041  heicant  28267  filnetlem4  28443  2rexrsb  29838  bnj580  31605  bnj852  31613
  Copyright terms: Public domain W3C validator