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

Theorem 2ralbii 2700
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 2698 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2698 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 2674
This theorem is referenced by:  cnvso  5378  fununi  5484  isocnv2  6018  tpossym  6478  sorpss  6494  dford2  7539  isffth2  14076  ispos2  14368  odulatb  14533  issubm  14711  cntzrec  15095  oppgsubm  15121  opprirred  15770  opprsubrg  15852  isbasis2g  16976  ist0-3  17371  isfbas2  17828  dfadj2  23349  adjval2  23355  cnlnadjeui  23541  adjbdln  23547  rmo4f  23945  isarchi  24213  iccllyscon  24898  dfso3  25138  elpotr  25359  dfon2  25370  f1opr  26324  fphpd  26775  isdomn3  27399  2reu4a  27842  dff14a  27967  ordelordALT  28341  isltrn2N  30614
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 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-ral 2679
  Copyright terms: Public domain W3C validator