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  4335  soeq1  4351  isoeq1  5849  isoeq2  5850  isoeq3  5851  fnmpoovd  6274  smoeq  6349  xpf1o  6906  tapeq1  7321  elinp  7543  cauappcvgpr  7731  seq3caopr2  10587  seqcaopr2g  10588  addcn2  11477  mulcn2  11479  sgrp1  13064  ismhm  13103  mhmex  13104  issubm  13114  isnsg  13342  nmznsg  13353  isghm  13383  iscmn  13433  ring1  13625  opprsubrngg  13777  issubrg3  13813  islmod  13857  lmodlema  13858  lsssetm  13922  islssmd  13925  islidlm  14045  ispsmet  14569  ismet  14590  isxmet  14591  addcncntoplem  14807  elcncf  14819  mpodvdsmulf1o  15236