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  5941  isoeq2  5942  isoeq3  5943  fnmpoovd  6379  smoeq  6455  xpf1o  7029  tapeq1  7470  elinp  7693  cauappcvgpr  7881  seq3caopr2  10754  seqcaopr2g  10755  wrd2ind  11303  addcn2  11870  mulcn2  11872  sgrp1  13493  ismhm  13543  mhmex  13544  issubm  13554  isnsg  13788  nmznsg  13799  isghm  13829  iscmn  13879  ring1  14071  opprsubrngg  14224  issubrg3  14260  islmod  14304  lmodlema  14305  lsssetm  14369  islssmd  14372  islidlm  14492  ispsmet  15046  ismet  15067  isxmet  15068  addcncntoplem  15284  elcncf  15296  mpodvdsmulf1o  15713