Theorem 2ralbidv 2518

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  cbvral3v  2741  poeq1  4330  soeq1  4346  isoeq1  5844  isoeq2  5845  isoeq3  5846  fnmpoovd  6268  smoeq  6343  xpf1o  6900  tapeq1  7312  elinp  7534  cauappcvgpr  7722  seq3caopr2  10564  seqcaopr2g  10565  addcn2  11453  mulcn2  11455  sgrp1  12994  ismhm  13033  mhmex  13034  issubm  13044  isnsg  13272  nmznsg  13283  isghm  13313  iscmn  13363  ring1  13555  opprsubrngg  13707  issubrg3  13743  islmod  13787  lmodlema  13788  lsssetm  13852  islssmd  13855  islidlm  13975  ispsmet  14491  ismet  14512  isxmet  14513  addcncntoplem  14719  elcncf  14728