Theorem raleqbidv 2744

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)

Hypotheses

Ref	Expression
raleqbidv.1	|- ( ph -> A = B )
raleqbidv.2	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
raleqbidv	|- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Distinct variable groups:   x, A   x, B   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem raleqbidv

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . 3 |- ( ph -> A = B )
2	1	raleqdv 2734	. 2 |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	ralbidv 2530	. 2 |- ( ph -> ( A. x e. B ps <-> A. x e. B ch ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   A.wral 2508

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-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  rspc2vd  3194  ofrfval  6239  fmpox  6360  tfrlemi1  6493  supeq123d  7181  acneq  7407  cvg1nlemcau  11535  cvg1nlemres  11536  cau3lem  11665  fsum2dlemstep  11985  fisumcom2  11989  fprod2dlemstep  12173  fprodcom2fi  12177  pcfac  12913  ptex  13337  prdsex  13342  prdsval  13346  ismgm  13430  mgm1  13443  grpidvalg  13446  gsumress  13468  issgrp  13476  sgrp1  13484  sgrppropd  13486  ismnddef  13491  ismndd  13510  mndpropd  13513  mnd1  13528  ismhm  13534  mhmex  13535  resmhm  13560  isgrp  13579  grppropd  13590  isgrpd2e  13593  grp1  13679  isnsg  13779  nmznsg  13790  isghm  13820  cmnpropd  13872  iscmnd  13875  isrng  13937  rngpropd  13958  dfur2g  13965  issrg  13968  issrgid  13984  isring  14003  iscrng2  14018  ringideu  14020  isringid  14028  ringpropd  14041  ring1  14062  oppr0g  14084  oppr1g  14085  isrhm2d  14169  rhmopp  14180  islring  14196  rrgval  14266  isdomn  14273  opprdomnbg  14278  islmod  14295  islmodd  14297  lmodprop2d  14352  lsssetm  14360  islidlm  14483  rnglidlmmgm  14500  rnglidlmsgrp  14501  mplvalcoe  14694  istopg  14713  restbasg  14882  cnfval  14908  cnpfval  14909  txbas  14972  limccl  15373  iswlk  16120  isclwwlk  16189  sscoll2  16519