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

Theorem r19.21v 2848
Description: Restricted quantifier version of 19.21v 1716. (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 361 . . . 4  |-  ( ( x  e.  A  -> 
( ph  ->  ps )
)  <->  ( ph  ->  ( x  e.  A  ->  ps ) ) )
21albii 1627 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  A. x
( ph  ->  ( x  e.  A  ->  ps ) ) )
3 19.21v 1716 . . 3  |-  ( A. x ( ph  ->  ( x  e.  A  ->  ps ) )  <->  ( ph  ->  A. x ( x  e.  A  ->  ps ) ) )
42, 3bitri 249 . 2  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  ( ph  ->  A. x ( x  e.  A  ->  ps ) ) )
5 df-ral 2798 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x
( x  e.  A  ->  ( ph  ->  ps ) ) )
6 df-ral 2798 . . 3  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
76imbi2i 312 . 2  |-  ( (
ph  ->  A. x  e.  A  ps )  <->  ( ph  ->  A. x ( x  e.  A  ->  ps )
) )
84, 5, 73bitr4i 277 1  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  ( ph  ->  A. x  e.  A  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1381    e. wcel 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-ex 1600  df-ral 2798
This theorem is referenced by:  r19.23v  2923  r19.32v  2989  rmo4  3278  2reu5lem3  3293  ra4v  3409  rmo3  3415  dftr5  4533  reusv3  4645  tfinds2  6683  tfinds3  6684  tfrlem1  7047  tfr3  7070  oeordi  7238  ordiso2  7943  ordtypelem7  7952  cantnf  8115  cantnfOLD  8137  dfac12lem3  8528  ttukeylem5  8896  ttukeylem6  8897  fpwwe2lem8  9018  grudomon  9198  raluz2  11141  ndvdssub  14047  gcdcllem1  14131  acsfn2  15042  pgpfac1  17110  pgpfac  17114  isdomn2  17927  islindf4  18851  isclo2  19567  1stccn  19942  kgencn  20035  txflf  20485  fclsopn  20493  nn0min  27589  rdgprc  29203  wfr3g  29318  bpolycl  29790  heicant  30025  filnetlem4  30175  2rexrsb  32130  bnj580  33839  bnj852  33847
  Copyright terms: Public domain W3C validator