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  6315  fmpox  6440  tfrlemi1  6607  supeq123d  7337  acneq  7564  cvg1nlemcau  11772  cvg1nlemres  11773  cau3lem  11903  fsum2dlemstep  12226  fisumcom2  12230  fprod2dlemstep  12414  fprodcom2fi  12418  pcfac  13158  ptex  13677  ismgm  13736  mgm1  13749  grpidvalg  13752  gzsumress  13771  issgrp  13777  sgrp1  13785  sgrppropd  13787  ismnddef  13790  ismndd  13809  mndpropd  13812  mnd1  13821  ismhm  13827  mhmex  13828  resmhm  13853  isgrp  13870  grppropd  13881  isgrpd2e  13884  grp1  13970  isnsg  14064  nmznsg  14075  isghm  14105  cmnpropd  14188  iscmnd  14191  prdsex  14279  prdsval  14280  isrng  14340  rngpropd  14361  dfur2g  14373  issrg  14376  issrgid  14392  isring  14411  iscrng2  14426  ringideu  14428  isringid  14437  ringpropd  14450  ring1  14471  oppr0g  14496  oppr1g  14497  isrhm2d  14581  rhmopp  14592  islring  14608  opprlring  14613  rrgval  14679  isdomn  14687  opprdomnbg  14692  islmod  14736  islmodd  14738  lmodprop2d  14794  lsssetm  14802  islidlm  14925  rnglidlmmgm  14942  rnglidlmsgrp  14943  isassa  15111  isassad  15120  assapropd  15123  mplvalcoe  15206  istopg  15225  restbasg  15394  cnfval  15420  cnpfval  15421  txbas  15484  limccl  15885  iswlk  16769  isclwwlk  16840  sscoll2  17219