Theorem 2ralbidv 2574

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  cbvral3v  2801  poeq1  4446  soeq1  4462  isoeq1  6010  isoeq2  6011  isoeq3  6012  fnmpoovd  6455  smoeq  6565  xpf1o  7149  papeq1  7616  papcotr  7620  tapeq1  7625  elinp  7848  cauappcvgpr  8036  seq3caopr2  10952  seqcaopr2g  10953  wrd2ind  11518  addcn2  12102  mulcn2  12104  sgrp1  13786  ismhm  13828  mhmex  13829  issubm  13839  isnsg  14065  nmznsg  14076  isghm  14106  iscmn  14187  ring1  14472  opprsubrngg  14629  issubrg3  14665  islmod  14737  lmodlema  14738  lsssetm  14803  islssmd  14806  islidlm  14926  ispsmet  15561  ismet  15582  isxmet  15583  addcncntoplem  15799  elcncf  15811  mpodvdsmulf1o  16296