Theorem 2ralbidv 2556

Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)

Hypothesis

Ref	Expression
2ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
2ralbidv	|- ( ph -> ( A. x e. A A. y e. B ps <-> A. x e. A A. y e. B ch ) )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)   ch( x, y)   A( x, y)   B( x, y)

Proof of Theorem 2ralbidv

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

Syntax hints:   -> wi 4   <-> wb 105   A.wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  cbvral3v  2782  poeq1  4396  soeq1  4412  isoeq1  5942  isoeq2  5943  isoeq3  5944  fnmpoovd  6380  smoeq  6456  xpf1o  7030  tapeq1  7471  elinp  7694  cauappcvgpr  7882  seq3caopr2  10755  seqcaopr2g  10756  wrd2ind  11304  addcn2  11871  mulcn2  11873  sgrp1  13495  ismhm  13545  mhmex  13546  issubm  13556  isnsg  13790  nmznsg  13801  isghm  13831  iscmn  13881  ring1  14074  opprsubrngg  14227  issubrg3  14263  islmod  14307  lmodlema  14308  lsssetm  14372  islssmd  14375  islidlm  14495  ispsmet  15049  ismet  15070  isxmet  15071  addcncntoplem  15287  elcncf  15299  mpodvdsmulf1o  15716