Theorem 2ralbidv 2514

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473

This theorem is referenced by:  cbvral3v  2733  poeq1  4314  soeq1  4330  isoeq1  5818  isoeq2  5819  isoeq3  5820  fnmpoovd  6234  smoeq  6309  xpf1o  6862  tapeq1  7269  elinp  7491  cauappcvgpr  7679  seq3caopr2  10500  addcn2  11336  mulcn2  11338  sgrp1  12840  ismhm  12879  mhmex  12880  issubm  12890  isnsg  13107  nmznsg  13118  isghm  13143  iscmn  13193  ring1  13372  opprsubrngg  13519  issubrg3  13555  islmod  13568  lmodlema  13569  lsssetm  13633  islssmd  13636  islidlm  13756  ispsmet  14220  ismet  14241  isxmet  14242  addcncntoplem  14448  elcncf  14457