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

Theorem 2ralbii 2899
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 2898 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2898 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 184   A.wral 2817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ral 2822
This theorem is referenced by:  cnvso  5552  fununi  5660  dff14a  6176  isocnv2  6226  sorpss  6580  tpossym  6999  dford2  8049  isffth2  15160  ispos2  15452  issubm  15850  cntzrec  16243  oppgsubm  16269  opprirred  17223  opprsubrg  17321  gsummatr01lem3  19028  gsummatr01  19030  isbasis2g  19318  ist0-3  19714  isfbas2  20204  dfadj2  26627  adjval2  26633  cnlnadjeui  26819  adjbdln  26825  rmo4f  27219  isarchi  27550  iccllyscon  28520  dfso3  28922  elpotr  29140  dfon2  29151  f1opr  30142  fphpd  30678  isdomn3  31093  2reu4a  31984  ordelordALT  32789  isltrn2N  35317  fiinfi  37179
  Copyright terms: Public domain W3C validator