Theorem 2ralbii 2832

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

Step	Hyp	Ref	Expression
1		ralbii.1	. . 3 |- ( ph <-> ps )
2	1	ralbii 2831	. 2 |- ( A. y e. B ph <-> A. y e. B ps )
3	2	ralbii 2831	1 |- ( A. x e. A A. y e. B ph <-> A. x e. A A. y e. B ps )

Syntax hints:   <-> wb 189   A.wral 2749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693

This theorem depends on definitions:  df-bi 190  df-ral 2754

This theorem is referenced by:  cnvso  5398  fununi  5675  dff14a  6200  isocnv2  6252  sorpss  6608  tpossym  7036  dford2  8156  isffth2  15876  ispos2  16248  issubm  16649  cntzrec  17042  oppgsubm  17068  opprirred  17985  opprsubrg  18084  gsummatr01lem3  19737  gsummatr01  19739  isbasis2g  20018  ist0-3  20416  isfbas2  20905  dfadj2  27594  adjval2  27600  cnlnadjeui  27786  adjbdln  27792  rmo4f  28189  isarchi  28550  iccllyscon  30023  dfso3  30402  elpotr  30477  dfon2  30488  f1opr  32097  isltrn2N  33731  fphpd  35705  isdomn3  36127  fiinfi  36223  ordelordALT  36943  2reu4a  38745  issubmgm  40158