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

Theorem r19.21v 2787
Description: Restricted quantifier version of 19.21v 1737. (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 359 . . . 4  |-  ( ( x  e.  A  -> 
( ph  ->  ps )
)  <->  ( ph  ->  ( x  e.  A  ->  ps ) ) )
21albii 1648 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  A. x
( ph  ->  ( x  e.  A  ->  ps ) ) )
3 19.21v 1737 . . 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 2737 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x
( x  e.  A  ->  ( ph  ->  ps ) ) )
6 df-ral 2737 . . 3  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
76imbi2i 310 . 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 1397    e. wcel 1826   A.wral 2732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712
This theorem depends on definitions:  df-bi 185  df-ex 1621  df-ral 2737
This theorem is referenced by:  r19.23v  2862  r19.32v  2928  rmo4  3217  2reu5lem3  3232  ra4v  3337  rmo3  3343  dftr5  4463  reusv3  4573  tfinds2  6597  tfinds3  6598  tfrlem1  6963  tfr3  6986  oeordi  7154  ordiso2  7855  ordtypelem7  7864  cantnf  8025  cantnfOLD  8047  dfac12lem3  8438  ttukeylem5  8806  ttukeylem6  8807  fpwwe2lem8  8926  grudomon  9106  raluz2  11050  ndvdssub  14067  gcdcllem1  14151  acsfn2  15070  pgpfac1  17244  pgpfac  17248  isdomn2  18061  islindf4  18958  isclo2  19675  1stccn  20049  kgencn  20142  txflf  20592  fclsopn  20600  nn0min  27764  rdgprc  29392  wfr3g  29507  bpolycl  29967  heicant  30214  filnetlem4  30365  2rexrsb  32342  bnj580  34318  bnj852  34326
  Copyright terms: Public domain W3C validator