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  5805  isoeq2  5806  isoeq3  5807  fnmpoovd  6219  smoeq  6294  xpf1o  6847  tapeq1  7254  elinp  7476  cauappcvgpr  7664  seq3caopr2  10485  addcn2  11321  mulcn2  11323  sgrp1  12823  ismhm  12861  issubm  12871  isnsg  13076  nmznsg  13087  iscmn  13111  ring1  13274  issubrg3  13406  islmod  13419  lmodlema  13420  lsssetm  13482  islssmd  13484  ispsmet  14011  ismet  14032  isxmet  14033  addcncntoplem  14239  elcncf  14248