Theorem raleqbidv 2759

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 2749	. 2 |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	ralbidv 2544	. 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 1398   A.wral 2522

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527

This theorem is referenced by:  rspc2vd  3209  ofrfval  6277  fmpox  6398  tfrlemi1  6565  supeq123d  7284  acneq  7511  cvg1nlemcau  11673  cvg1nlemres  11674  cau3lem  11803  fsum2dlemstep  12124  fisumcom2  12128  fprod2dlemstep  12312  fprodcom2fi  12316  pcfac  13052  ptex  13494  prdsex  13499  prdsval  13503  ismgm  13587  mgm1  13600  grpidvalg  13603  gsumress  13625  issgrp  13633  sgrp1  13641  sgrppropd  13643  ismnddef  13648  ismndd  13667  mndpropd  13670  mnd1  13685  ismhm  13691  mhmex  13692  resmhm  13717  isgrp  13736  grppropd  13747  isgrpd2e  13750  grp1  13836  isnsg  13936  nmznsg  13947  isghm  13977  cmnpropd  14029  iscmnd  14032  isrng  14095  rngpropd  14116  dfur2g  14123  issrg  14126  issrgid  14142  isring  14161  iscrng2  14176  ringideu  14178  isringid  14186  ringpropd  14199  ring1  14220  oppr0g  14242  oppr1g  14243  isrhm2d  14327  rhmopp  14338  islring  14354  rrgval  14424  isdomn  14432  opprdomnbg  14437  islmod  14456  islmodd  14458  lmodprop2d  14513  lsssetm  14521  islidlm  14644  rnglidlmmgm  14661  rnglidlmsgrp  14662  mplvalcoe  14862  istopg  14881  restbasg  15050  cnfval  15076  cnpfval  15077  txbas  15140  limccl  15541  iswlk  16335  isclwwlk  16406  sscoll2  16775