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

Theorem r19.21v 2592
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 2591 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 2509
This theorem is referenced by:  r19.32v  2648  rmo4  2897  rmo3  3006  dftr5  4013  reusv3  4433  tfinds2  4545  tfinds3  4546  tfr3  6301  oeordi  6471  ordiso2  7114  ordtypelem7  7123  cantnf  7279  dfac12lem3  7655  ttukeylem5  8024  ttukeylem6  8025  fpwwe2lem8  8139  grudomon  8319  raluz2  10147  ndvdssub  12480  gcdcllem1  12564  acsfn2  13409  pgpfac1  15150  pgpfac  15154  isdomn2  15872  isclo2  16657  1stccn  17021  kgencn  17083  txflf  17533  fclsopn  17541  rdgprc  23319  wfr3g  23423  bpolycl  23961  filnetlem4  25496  islindf4  26474  bnj580  27634  bnj852  27642
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 2513
  Copyright terms: Public domain W3C validator