Theorem 2ralbii 2735

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-ral 2714

This theorem is referenced by:  cnvso  5369  fununi  5477  isocnv2  6015  sorpss  6360  tpossym  6772  dford2  7818  isffth2  14818  ispos2  15110  issubm  15466  cntzrec  15840  oppgsubm  15866  opprirred  16780  opprsubrg  16862  gsummatr01lem3  18432  gsummatr01  18434  isbasis2g  18522  ist0-3  18918  isfbas2  19377  dfadj2  25234  adjval2  25240  cnlnadjeui  25426  adjbdln  25432  rmo4f  25826  isarchi  26144  iccllyscon  27087  dfso3  27323  elpotr  27541  dfon2  27552  f1opr  28561  fphpd  29098  isdomn3  29515  2reu4a  29956  dff14a  30087  ordelordALT  31101  isltrn2N  33515