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

Theorem 2ralbii 2677
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 2675 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2675 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 177   A.wral 2651
This theorem is referenced by:  cnvso  5353  fununi  5459  isocnv2  5992  tpossym  6449  sorpss  6465  dford2  7510  isffth2  14042  ispos2  14334  odulatb  14499  issubm  14677  cntzrec  15061  oppgsubm  15087  opprirred  15736  opprsubrg  15818  isbasis2g  16938  ist0-3  17333  isfbas2  17790  dfadj2  23238  adjval2  23244  cnlnadjeui  23430  adjbdln  23436  rmo4f  23830  iccllyscon  24718  dfso3  24958  elpotr  25163  dfon2  25174  f1opr  26119  fphpd  26570  isdomn3  27194  2reu4a  27637  ordelordALT  27967  isltrn2N  30236
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-ral 2656
  Copyright terms: Public domain W3C validator