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

Theorem 2ralbii 2733
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 2731 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2731 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 178   A.wral 2707
This theorem is referenced by:  cnvso  5414  fununi  5520  isocnv2  6054  tpossym  6514  sorpss  6530  dford2  7578  isffth2  14118  ispos2  14410  odulatb  14575  issubm  14753  cntzrec  15137  oppgsubm  15163  opprirred  15812  opprsubrg  15894  isbasis2g  17018  ist0-3  17414  isfbas2  17872  dfadj2  23393  adjval2  23399  cnlnadjeui  23585  adjbdln  23591  rmo4f  23989  isarchi  24257  iccllyscon  24942  dfso3  25182  elpotr  25413  dfon2  25424  f1opr  26440  fphpd  26891  isdomn3  27514  2reu4a  27957  dff14a  28096  ordelordALT  28696  isltrn2N  30991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-ral 2712
  Copyright terms: Public domain W3C validator