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

Theorem r19.21v 2869
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.) 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 1620 . . 3  |-  ( A. x ( x  e.  A  ->  ( ph  ->  ps ) )  <->  A. x
( ph  ->  ( x  e.  A  ->  ps ) ) )
3 19.21v 1930 . . 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 2819 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  <->  A. x
( x  e.  A  ->  ( ph  ->  ps ) ) )
6 df-ral 2819 . . 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 1377    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-ral 2819
This theorem is referenced by:  r19.23v  2943  r19.32v  3007  rmo4  3296  2reu5lem3  3311  rmo3  3430  dftr5  4543  reusv3  4655  tfinds2  6676  tfinds3  6677  tfrlem1  7042  tfr3  7065  oeordi  7233  ordiso2  7936  ordtypelem7  7945  cantnf  8108  cantnfOLD  8130  dfac12lem3  8521  ttukeylem5  8889  ttukeylem6  8890  fpwwe2lem8  9011  grudomon  9191  raluz2  11126  ndvdssub  13920  gcdcllem1  14004  acsfn2  14914  pgpfac1  16921  pgpfac  16925  isdomn2  17719  islindf4  18640  isclo2  19355  1stccn  19730  kgencn  19792  txflf  20242  fclsopn  20250  nn0min  27279  rdgprc  28804  wfr3g  28919  bpolycl  29391  heicant  29626  filnetlem4  29802  2rexrsb  31643  bnj580  33050  bnj852  33058
  Copyright terms: Public domain W3C validator