Theorem 2ralbii 2899

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 2898	. 2 |- ( A. y e. B ph <-> A. y e. B ps )
3	2	ralbii 2898	1 |- ( A. x e. A A. y e. B ph <-> A. x e. A A. y e. B ps )

Syntax hints:   <-> wb 184   A.wral 2817

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

This theorem depends on definitions:  df-bi 185  df-ral 2822

This theorem is referenced by:  cnvso  5552  fununi  5660  dff14a  6176  isocnv2  6226  sorpss  6580  tpossym  6999  dford2  8049  isffth2  15160  ispos2  15452  issubm  15850  cntzrec  16243  oppgsubm  16269  opprirred  17223  opprsubrg  17321  gsummatr01lem3  19028  gsummatr01  19030  isbasis2g  19318  ist0-3  19714  isfbas2  20204  dfadj2  26627  adjval2  26633  cnlnadjeui  26819  adjbdln  26825  rmo4f  27219  isarchi  27550  iccllyscon  28520  dfso3  28922  elpotr  29140  dfon2  29151  f1opr  30142  fphpd  30678  isdomn3  31093  2reu4a  31984  ordelordALT  32789  isltrn2N  35317  fiinfi  37179