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

Theorem 2ralbii 2832
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 2831 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2831 1  |-  ( 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 189   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693
This theorem depends on definitions:  df-bi 190  df-ral 2754
This theorem is referenced by:  cnvso  5398  fununi  5675  dff14a  6200  isocnv2  6252  sorpss  6608  tpossym  7036  dford2  8156  isffth2  15876  ispos2  16248  issubm  16649  cntzrec  17042  oppgsubm  17068  opprirred  17985  opprsubrg  18084  gsummatr01lem3  19737  gsummatr01  19739  isbasis2g  20018  ist0-3  20416  isfbas2  20905  dfadj2  27594  adjval2  27600  cnlnadjeui  27786  adjbdln  27792  rmo4f  28189  isarchi  28550  iccllyscon  30023  dfso3  30402  elpotr  30477  dfon2  30488  f1opr  32097  isltrn2N  33731  fphpd  35705  isdomn3  36127  fiinfi  36223  ordelordALT  36943  2reu4a  38745  issubmgm  40158
  Copyright terms: Public domain W3C validator