Theorem 2ralbidv 2530

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  cbvral3v  2753  poeq1  4347  soeq1  4363  isoeq1  5872  isoeq2  5873  isoeq3  5874  fnmpoovd  6303  smoeq  6378  xpf1o  6943  tapeq1  7366  elinp  7589  cauappcvgpr  7777  seq3caopr2  10640  seqcaopr2g  10641  addcn2  11654  mulcn2  11656  sgrp1  13276  ismhm  13326  mhmex  13327  issubm  13337  isnsg  13571  nmznsg  13582  isghm  13612  iscmn  13662  ring1  13854  opprsubrngg  14006  issubrg3  14042  islmod  14086  lmodlema  14087  lsssetm  14151  islssmd  14154  islidlm  14274  ispsmet  14828  ismet  14849  isxmet  14850  addcncntoplem  15066  elcncf  15078  mpodvdsmulf1o  15495