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

Theorem 2ralbii 2723
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 2721 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2721 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 2697
This theorem is referenced by:  cnvso  5403  fununi  5509  isocnv2  6043  tpossym  6503  sorpss  6519  dford2  7565  isffth2  14103  ispos2  14395  odulatb  14560  issubm  14738  cntzrec  15122  oppgsubm  15148  opprirred  15797  opprsubrg  15879  isbasis2g  17003  ist0-3  17399  isfbas2  17857  dfadj2  23378  adjval2  23384  cnlnadjeui  23570  adjbdln  23576  rmo4f  23974  isarchi  24242  iccllyscon  24927  dfso3  25167  elpotr  25396  dfon2  25407  f1opr  26380  fphpd  26831  isdomn3  27455  2reu4a  27898  dff14a  28028  ordelordALT  28523  isltrn2N  30818
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator