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

Theorem 2ralbii 2838
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 2837 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2837 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 186   A.wral 2756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654
This theorem depends on definitions:  df-bi 187  df-ral 2761
This theorem is referenced by:  cnvso  5365  fununi  5637  dff14a  6160  isocnv2  6212  sorpss  6569  tpossym  6992  dford2  8072  isffth2  15531  ispos2  15903  issubm  16304  cntzrec  16697  oppgsubm  16723  opprirred  17673  opprsubrg  17772  gsummatr01lem3  19453  gsummatr01  19455  isbasis2g  19743  ist0-3  20141  isfbas2  20630  dfadj2  27230  adjval2  27236  cnlnadjeui  27422  adjbdln  27428  rmo4f  27824  isarchi  28191  iccllyscon  29560  dfso3  29939  elpotr  30013  dfon2  30024  f1opr  31510  isltrn2N  33150  fphpd  35124  isdomn3  35541  fiinfi  35637  ordelordALT  36341  2reu4a  37575  issubmgm  38119
  Copyright terms: Public domain W3C validator