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

Theorem r19.21v 2785
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 2784 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wral 2697
This theorem is referenced by:  r19.32v  2846  rmo4  3119  2reu5lem3  3133  rmo3  3240  dftr5  4297  reusv3  4722  tfinds2  4834  tfinds3  4835  tfr3  6651  oeordi  6821  ordiso2  7473  ordtypelem7  7482  cantnf  7638  dfac12lem3  8014  ttukeylem5  8382  ttukeylem6  8383  fpwwe2lem8  8501  grudomon  8681  raluz2  10515  ndvdssub  12915  gcdcllem1  12999  acsfn2  13876  pgpfac1  15626  pgpfac  15630  isdomn2  16347  isclo2  17140  1stccn  17514  kgencn  17576  txflf  18026  fclsopn  18034  rdgprc  25406  wfr3g  25510  bpolycl  26046  filnetlem4  26347  islindf4  27223  2rexrsb  27863  bnj580  29138  bnj852  29146
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator