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

Theorem r19.21v 2805
Description: Restricted quantifier version of 19.21v 1797. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.)
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 bi2.04 367 . . . 4  |-  ( ( x  e.  A  -> 
( ph  ->  ps )
)  <->  ( ph  ->  ( x  e.  A  ->  ps ) ) )
21albii 1702 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  A. x
( ph  ->  ( x  e.  A  ->  ps ) ) )
3 19.21v 1797 . . 3  |-  ( A. x ( ph  ->  ( x  e.  A  ->  ps ) )  <->  ( ph  ->  A. x ( x  e.  A  ->  ps ) ) )
42, 3bitri 257 . 2  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  ( ph  ->  A. x ( x  e.  A  ->  ps ) ) )
5 df-ral 2754 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x
( x  e.  A  ->  ( ph  ->  ps ) ) )
6 df-ral 2754 . . 3  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
76imbi2i 318 . 2  |-  ( (
ph  ->  A. x  e.  A  ps )  <->  ( ph  ->  A. x ( x  e.  A  ->  ps )
) )
84, 5, 73bitr4i 285 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1453    e. wcel 1898   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769
This theorem depends on definitions:  df-bi 190  df-ex 1675  df-ral 2754
This theorem is referenced by:  r19.23v  2879  r19.32v  2948  rmo4  3243  2reu5lem3  3259  ra4v  3364  rmo3  3370  dftr5  4514  reusv3  4625  tfinds2  6717  tfinds3  6718  wfr3g  7060  tfrlem1  7120  tfr3  7143  oeordi  7314  ordiso2  8056  ordtypelem7  8065  cantnf  8224  dfac12lem3  8601  ttukeylem5  8969  ttukeylem6  8970  fpwwe2lem8  9088  grudomon  9268  raluz2  11237  bpolycl  14154  ndvdssub  14437  gcdcllem1  14522  acsfn2  15618  pgpfac1  17762  pgpfac  17766  isdomn2  18572  islindf4  19445  isclo2  20153  1stccn  20527  kgencn  20620  txflf  21070  fclsopn  21078  nn0min  28433  bnj580  29773  bnj852  29781  rdgprc  30490  filnetlem4  31086  poimirlem29  32014  heicant  32020  2rexrsb  38630
  Copyright terms: Public domain W3C validator