Theorem 2ralbidv 2521

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  cbvral3v  2744  poeq1  4334  soeq1  4350  isoeq1  5848  isoeq2  5849  isoeq3  5850  fnmpoovd  6273  smoeq  6348  xpf1o  6905  tapeq1  7319  elinp  7541  cauappcvgpr  7729  seq3caopr2  10585  seqcaopr2g  10586  addcn2  11475  mulcn2  11477  sgrp1  13054  ismhm  13093  mhmex  13094  issubm  13104  isnsg  13332  nmznsg  13343  isghm  13373  iscmn  13423  ring1  13615  opprsubrngg  13767  issubrg3  13803  islmod  13847  lmodlema  13848  lsssetm  13912  islssmd  13915  islidlm  14035  ispsmet  14559  ismet  14580  isxmet  14581  addcncntoplem  14797  elcncf  14809  mpodvdsmulf1o  15226