Theorem 2ralbii 2838

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

Syntax hints:   <-> wb 186   A.wral 2756

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

This theorem depends on definitions:  df-bi 187  df-ral 2761

This theorem is referenced by:  cnvso  5365  fununi  5637  dff14a  6160  isocnv2  6212  sorpss  6569  tpossym  6992  dford2  8072  isffth2  15531  ispos2  15903  issubm  16304  cntzrec  16697  oppgsubm  16723  opprirred  17673  opprsubrg  17772  gsummatr01lem3  19453  gsummatr01  19455  isbasis2g  19743  ist0-3  20141  isfbas2  20630  dfadj2  27230  adjval2  27236  cnlnadjeui  27422  adjbdln  27428  rmo4f  27824  isarchi  28191  iccllyscon  29560  dfso3  29939  elpotr  30013  dfon2  30024  f1opr  31510  isltrn2N  33150  fphpd  35124  isdomn3  35541  fiinfi  35637  ordelordALT  36341  2reu4a  37575  issubmgm  38119