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

Theorem r19.21v 2770
Description: Restricted quantifier version of 19.21v 1779. (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 362 . . . 4  |-  ( ( x  e.  A  -> 
( ph  ->  ps )
)  <->  ( ph  ->  ( x  e.  A  ->  ps ) ) )
21albii 1685 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  A. x
( ph  ->  ( x  e.  A  ->  ps ) ) )
3 19.21v 1779 . . 3  |-  ( A. x ( ph  ->  ( x  e.  A  ->  ps ) )  <->  ( ph  ->  A. x ( x  e.  A  ->  ps ) ) )
42, 3bitri 252 . 2  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  ( ph  ->  A. x ( x  e.  A  ->  ps ) ) )
5 df-ral 2719 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x
( x  e.  A  ->  ( ph  ->  ps ) ) )
6 df-ral 2719 . . 3  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
76imbi2i 313 . 2  |-  ( (
ph  ->  A. x  e.  A  ps )  <->  ( ph  ->  A. x ( x  e.  A  ->  ps )
) )
84, 5, 73bitr4i 280 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435    e. wcel 1872   A.wral 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-ex 1658  df-ral 2719
This theorem is referenced by:  r19.23v  2844  r19.32v  2913  rmo4  3206  2reu5lem3  3222  ra4v  3327  rmo3  3333  dftr5  4464  reusv3  4575  tfinds2  6648  tfinds3  6649  wfr3g  6989  tfrlem1  7049  tfr3  7072  oeordi  7243  ordiso2  7983  ordtypelem7  7992  cantnf  8150  dfac12lem3  8526  ttukeylem5  8894  ttukeylem6  8895  fpwwe2lem8  9013  grudomon  9193  raluz2  11159  bpolycl  14048  ndvdssub  14331  gcdcllem1  14416  acsfn2  15512  pgpfac1  17656  pgpfac  17660  isdomn2  18466  islindf4  19338  isclo2  20046  1stccn  20420  kgencn  20513  txflf  20963  fclsopn  20971  nn0min  28335  bnj580  29676  bnj852  29684  rdgprc  30392  filnetlem4  30986  poimirlem29  31876  heicant  31882  2rexrsb  38406
  Copyright terms: Public domain W3C validator