Theorem raleqbidv 2765

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   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-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533

This theorem is used by:  rspc2vd  3216  ofrfval  6311  fmpox  6436  tfrlemi1  6603  supeq123d  7331  acneq  7558  cvg1nlemcau  11750  cvg1nlemres  11751  cau3lem  11880  fsum2dlemstep  12201  fisumcom2  12205  fprod2dlemstep  12389  fprodcom2fi  12393  pcfac  13129  ptex  13618  ismgm  13677  mgm1  13690  grpidvalg  13693  gzsumress  13712  issgrp  13718  sgrp1  13726  sgrppropd  13728  ismnddef  13731  ismndd  13750  mndpropd  13753  mnd1  13762  ismhm  13768  mhmex  13769  resmhm  13794  isgrp  13811  grppropd  13822  isgrpd2e  13825  grp1  13911  isnsg  14005  nmznsg  14016  isghm  14046  cmnpropd  14098  iscmnd  14101  prdsex  14172  prdsval  14173  isrng  14233  rngpropd  14254  dfur2g  14266  issrg  14269  issrgid  14285  isring  14304  iscrng2  14319  ringideu  14321  isringid  14330  ringpropd  14343  ring1  14364  oppr0g  14387  oppr1g  14388  isrhm2d  14472  rhmopp  14483  islring  14499  opprlring  14504  rrgval  14570  isdomn  14578  opprdomnbg  14583  islmod  14627  islmodd  14629  lmodprop2d  14685  lsssetm  14693  islidlm  14816  rnglidlmmgm  14833  rnglidlmsgrp  14834  isassa  15002  isassad  15011  assapropd  15014  mplvalcoe  15081  istopg  15100  restbasg  15269  cnfval  15295  cnpfval  15296  txbas  15359  limccl  15760  iswlk  16564  isclwwlk  16635  sscoll2  17014