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

Theorem 2ralbii 2735
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 2733 . 2  |-  ( A. y  e.  B  ph  <->  A. y  e.  B  ps )
32ralbii 2733 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 2709
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 2714
This theorem is referenced by:  cnvso  5369  fununi  5477  isocnv2  6015  sorpss  6360  tpossym  6772  dford2  7818  isffth2  14818  ispos2  15110  issubm  15466  cntzrec  15840  oppgsubm  15866  opprirred  16780  opprsubrg  16862  gsummatr01lem3  18432  gsummatr01  18434  isbasis2g  18522  ist0-3  18918  isfbas2  19377  dfadj2  25234  adjval2  25240  cnlnadjeui  25426  adjbdln  25432  rmo4f  25826  isarchi  26144  iccllyscon  27087  dfso3  27323  elpotr  27541  dfon2  27552  f1opr  28561  fphpd  29098  isdomn3  29515  2reu4a  29956  dff14a  30087  ordelordALT  31101  isltrn2N  33515
  Copyright terms: Public domain W3C validator