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

Step	Hyp	Ref	Expression
1		ralbii.1	. . 3
2	1	ralbii 2888	. 2
3	2	ralbii 2888	1

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