Theorem 2ralbidv 2554

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 2530	. 2 |- ( ph -> ( A. y e. B ps <-> A. y e. B ch ) )
3	2	ralbidv 2530	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 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  cbvral3v  2780  poeq1  4390  soeq1  4406  isoeq1  5931  isoeq2  5932  isoeq3  5933  fnmpoovd  6367  smoeq  6442  xpf1o  7013  tapeq1  7449  elinp  7672  cauappcvgpr  7860  seq3caopr2  10727  seqcaopr2g  10728  wrd2ind  11271  addcn2  11837  mulcn2  11839  sgrp1  13460  ismhm  13510  mhmex  13511  issubm  13521  isnsg  13755  nmznsg  13766  isghm  13796  iscmn  13846  ring1  14038  opprsubrngg  14191  issubrg3  14227  islmod  14271  lmodlema  14272  lsssetm  14336  islssmd  14339  islidlm  14459  ispsmet  15013  ismet  15034  isxmet  15035  addcncntoplem  15251  elcncf  15263  mpodvdsmulf1o  15680