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

Theorem 2ralbii 2762
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 2760 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2760 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 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-ral 2741
This theorem is referenced by:  cnvso  5397  fununi  5505  isocnv2  6043  sorpss  6386  tpossym  6798  dford2  7847  isffth2  14847  ispos2  15139  issubm  15496  cntzrec  15872  oppgsubm  15898  opprirred  16816  opprsubrg  16908  gsummatr01lem3  18485  gsummatr01  18487  isbasis2g  18575  ist0-3  18971  isfbas2  19430  dfadj2  25311  adjval2  25317  cnlnadjeui  25503  adjbdln  25509  rmo4f  25903  isarchi  26221  iccllyscon  27161  dfso3  27398  elpotr  27616  dfon2  27627  f1opr  28644  fphpd  29181  isdomn3  29598  2reu4a  30039  dff14a  30170  ordelordALT  31340  isltrn2N  33860
  Copyright terms: Public domain W3C validator