MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2ralbii Unicode version

Theorem 2ralbii 2645
Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
Hypothesis
Ref Expression
ralbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
2ralbii  |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. x  e.  A  A. y  e.  B  ps )

Proof of Theorem 2ralbii
StepHypRef Expression
1 ralbii.1 . . 3  |-  ( ph  <->  ps )
21ralbii 2643 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2643 1  |-  ( A. x  e.  A  A. y  e.  B  ph  <->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wral 2619
This theorem is referenced by:  cnvso  5293  fununi  5395  isocnv2  5912  tpossym  6350  sorpss  6366  dford2  7408  ispos2  14175  odulatb  14340  issubm  14518  cntzrec  14902  oppgsubm  14928  opprirred  15577  opprsubrg  15659  isbasis2g  16786  ist0-3  17173  isfbas2  17626  dfadj2  22573  adjval2  22579  cnlnadjeui  22765  adjbdln  22771  rmo4f  23173  iccllyscon  24185  dfso3  24478  elpotr  24695  dfon2  24706  dfcon2OLD  25577  f1opr  25715  fphpd  26222  isdomn3  26846  2reu4a  27290  ordelordALT  28029  isltrn2N  30361
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-ral 2624
  Copyright terms: Public domain W3C validator