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

Theorem r19.21v 2601
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 2600 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 2516
This theorem is referenced by:  r19.32v  2657  rmo4  2911  rmo3  3020  dftr5  4056  reusv3  4479  tfinds2  4591  tfinds3  4592  tfr3  6348  oeordi  6518  ordiso2  7163  ordtypelem7  7172  cantnf  7328  dfac12lem3  7704  ttukeylem5  8073  ttukeylem6  8074  fpwwe2lem8  8192  grudomon  8372  raluz2  10200  ndvdssub  12533  gcdcllem1  12617  acsfn2  13492  pgpfac1  15242  pgpfac  15246  isdomn2  15967  isclo2  16752  1stccn  17116  kgencn  17178  txflf  17628  fclsopn  17636  rdgprc  23485  wfr3g  23589  bpolycl  24127  filnetlem4  25662  islindf4  26640  bnj580  27957  bnj852  27965
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 2520
  Copyright terms: Public domain W3C validator