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

Theorem 2ralbii 2889
Description: Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
Hypothesis
Ref Expression
ralbii.1
Assertion
Ref Expression
2ralbii

Proof of Theorem 2ralbii
StepHypRef Expression
1 ralbii.1 . . 3
21ralbii 2888 . 2
32ralbii 2888 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  A.wral 2807
This theorem is referenced by:  cnvso  5551  fununi  5659  dff14a  6177  isocnv2  6227  sorpss  6585  tpossym  7006  dford2  8058  isffth2  15285  ispos2  15577  issubm  15978  cntzrec  16371  oppgsubm  16397  opprirred  17351  opprsubrg  17450  gsummatr01lem3  19159  gsummatr01  19161  isbasis2g  19449  ist0-3  19846  isfbas2  20336  dfadj2  26804  adjval2  26810  cnlnadjeui  26996  adjbdln  27002  rmo4f  27396  isarchi  27726  iccllyscon  28695  dfso3  29097  elpotr  29213  dfon2  29224  f1opr  30215  fphpd  30750  isdomn3  31164  2reu4a  32194  issubmgm  32477  ordelordALT  33308  isltrn2N  35844  fiinfi  37758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator