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  4444  soeq1  4460  isoeq1  6007  isoeq2  6008  isoeq3  6009  fnmpoovd  6451  smoeq  6561  xpf1o  7144  papeq1  7610  papcotr  7614  tapeq1  7619  elinp  7842  cauappcvgpr  8030  seq3caopr2  10944  seqcaopr2g  10945  wrd2ind  11510  addcn2  12094  mulcn2  12096  sgrp1  13777  ismhm  13819  mhmex  13820  issubm  13830  isnsg  14056  nmznsg  14067  isghm  14097  iscmn  14147  ring1  14415  opprsubrngg  14570  issubrg3  14606  islmod  14678  lmodlema  14679  lsssetm  14744  islssmd  14747  islidlm  14867  ispsmet  15476  ismet  15497  isxmet  15498  addcncntoplem  15714  elcncf  15726  mpodvdsmulf1o  16206