MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.26-2 Structured version   Unicode version

Theorem r19.26-2 2982
Description: Restricted quantifier version of 19.26-2 1686. Version of r19.26 2981 with two quantifiers. (Contributed by NM, 10-Aug-2004.)
Assertion
Ref Expression
r19.26-2  |-  ( A. x  e.  A  A. y  e.  B  ( ph  /\  ps )  <->  ( A. x  e.  A  A. y  e.  B  ph  /\  A. x  e.  A  A. y  e.  B  ps ) )

Proof of Theorem r19.26-2
StepHypRef Expression
1 r19.26 2981 . . 3  |-  ( A. y  e.  B  ( ph  /\  ps )  <->  ( A. y  e.  B  ph  /\  A. y  e.  B  ps ) )
21ralbii 2885 . 2  |-  ( A. x  e.  A  A. y  e.  B  ( ph  /\  ps )  <->  A. x  e.  A  ( A. y  e.  B  ph  /\  A. y  e.  B  ps ) )
3 r19.26 2981 . 2  |-  ( A. x  e.  A  ( A. y  e.  B  ph 
/\  A. y  e.  B  ps )  <->  ( A. x  e.  A  A. y  e.  B  ph  /\  A. x  e.  A  A. y  e.  B  ps ) )
42, 3bitri 249 1  |-  ( A. x  e.  A  A. y  e.  B  ( ph  /\  ps )  <->  ( A. x  e.  A  A. y  e.  B  ph  /\  A. x  e.  A  A. y  e.  B  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-an 369  df-ral 2809
This theorem is referenced by:  fununi  5636  tz7.48lem  7098  isffth2  15404  ispos2  15776  issgrpv  16112  issgrpn0  16113  isnsg2  16430  efgred  16965  dfrhm2  17561  cpmatacl  19384  cpmatmcllem  19386  caucfil  21888  aalioulem6  22899  ajmoi  25972  adjmo  26949  iccllyscon  28959  dfso3  29338  ispridl2  30675  isrnghm  32952  ishlat2  35475  fiinfi  38171
  Copyright terms: Public domain W3C validator