Theorem 2ralbidv 2501

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  cbvral3v  2718  poeq1  4299  soeq1  4315  isoeq1  5801  isoeq2  5802  isoeq3  5803  fnmpoovd  6215  smoeq  6290  xpf1o  6843  tapeq1  7250  elinp  7472  cauappcvgpr  7660  seq3caopr2  10481  addcn2  11317  mulcn2  11319  sgrp1  12815  ismhm  12852  issubm  12862  isnsg  13060  nmznsg  13071  iscmn  13094  ring1  13234  issubrg3  13366  islmod  13379  lmodlema  13380  ispsmet  13793  ismet  13814  isxmet  13815  addcncntoplem  14021  elcncf  14030