Theorem 2ralbii 2762

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

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 2741

This theorem is referenced by:  cnvso  5397  fununi  5505  isocnv2  6043  sorpss  6386  tpossym  6798  dford2  7847  isffth2  14847  ispos2  15139  issubm  15496  cntzrec  15872  oppgsubm  15898  opprirred  16816  opprsubrg  16908  gsummatr01lem3  18485  gsummatr01  18487  isbasis2g  18575  ist0-3  18971  isfbas2  19430  dfadj2  25311  adjval2  25317  cnlnadjeui  25503  adjbdln  25509  rmo4f  25903  isarchi  26221  iccllyscon  27161  dfso3  27398  elpotr  27616  dfon2  27627  f1opr  28644  fphpd  29181  isdomn3  29598  2reu4a  30039  dff14a  30170  ordelordALT  31340  isltrn2N  33860