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  5851  isoeq2  5852  isoeq3  5853  fnmpoovd  6282  smoeq  6357  xpf1o  6914  tapeq1  7335  elinp  7558  cauappcvgpr  7746  seq3caopr2  10602  seqcaopr2g  10603  addcn2  11492  mulcn2  11494  sgrp1  13113  ismhm  13163  mhmex  13164  issubm  13174  isnsg  13408  nmznsg  13419  isghm  13449  iscmn  13499  ring1  13691  opprsubrngg  13843  issubrg3  13879  islmod  13923  lmodlema  13924  lsssetm  13988  islssmd  13991  islidlm  14111  ispsmet  14643  ismet  14664  isxmet  14665  addcncntoplem  14881  elcncf  14893  mpodvdsmulf1o  15310