Theorem 2ralbidv 2501

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  cbvral3v  2720  poeq1  4301  soeq1  4317  isoeq1  5804  isoeq2  5805  isoeq3  5806  fnmpoovd  6218  smoeq  6293  xpf1o  6846  tapeq1  7253  elinp  7475  cauappcvgpr  7663  seq3caopr2  10484  addcn2  11320  mulcn2  11322  sgrp1  12821  ismhm  12858  issubm  12868  isnsg  13067  nmznsg  13078  iscmn  13101  ring1  13241  issubrg3  13373  islmod  13386  lmodlema  13387  lsssetm  13449  islssmd  13451  ispsmet  13862  ismet  13883  isxmet  13884  addcncntoplem  14090  elcncf  14099