Theorem 2ralbidv 2566

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525

This theorem is referenced by:  cbvral3v  2792  poeq1  4419  soeq1  4435  isoeq1  5973  isoeq2  5974  isoeq3  5975  fnmpoovd  6410  smoeq  6520  xpf1o  7096  papcotr  7561  tapeq1  7565  elinp  7788  cauappcvgpr  7976  seq3caopr2  10854  seqcaopr2g  10855  wrd2ind  11411  addcn2  11991  mulcn2  11993  sgrp1  13616  ismhm  13666  mhmex  13667  issubm  13677  isnsg  13911  nmznsg  13922  isghm  13952  iscmn  14002  ring1  14195  opprsubrngg  14348  issubrg3  14384  islmod  14431  lmodlema  14432  lsssetm  14496  islssmd  14499  islidlm  14619  ispsmet  15180  ismet  15201  isxmet  15202  addcncntoplem  15418  elcncf  15430  mpodvdsmulf1o  15850