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

Theorem r19.21v 2643
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 1609 . 2  |-  F/ x ph
21r19.21 2642 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wral 2556
This theorem is referenced by:  r19.32v  2699  rmo4  2971  2reu5lem3  2985  rmo3  3091  dftr5  4132  reusv3  4558  tfinds2  4670  tfinds3  4671  tfr3  6431  oeordi  6601  ordiso2  7246  ordtypelem7  7255  cantnf  7411  dfac12lem3  7787  ttukeylem5  8156  ttukeylem6  8157  fpwwe2lem8  8275  grudomon  8455  raluz2  10284  ndvdssub  12622  gcdcllem1  12706  acsfn2  13581  pgpfac1  15331  pgpfac  15335  isdomn2  16056  isclo2  16841  1stccn  17205  kgencn  17267  txflf  17717  fclsopn  17725  rdgprc  24222  wfr3g  24326  bpolycl  24859  filnetlem4  26433  islindf4  27411  2rexrsb  28052  bnj580  29261  bnj852  29269
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator