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  3210  ofrfval  6284  fmpox  6409  tfrlemi1  6576  supeq123d  7295  acneq  7522  cvg1nlemcau  11694  cvg1nlemres  11695  cau3lem  11824  fsum2dlemstep  12145  fisumcom2  12149  fprod2dlemstep  12333  fprodcom2fi  12337  pcfac  13073  ptex  13561  ismgm  13620  mgm1  13633  grpidvalg  13636  gsumress  13658  issgrp  13666  sgrp1  13674  sgrppropd  13676  ismnddef  13679  ismndd  13698  mndpropd  13701  mnd1  13710  ismhm  13716  mhmex  13717  resmhm  13742  isgrp  13761  grppropd  13772  isgrpd2e  13775  grp1  13861  isnsg  13955  nmznsg  13966  isghm  13996  cmnpropd  14048  iscmnd  14051  prdsex  14114  prdsval  14115  isrng  14173  rngpropd  14194  dfur2g  14205  issrg  14208  issrgid  14224  isring  14243  iscrng2  14258  ringideu  14260  isringid  14268  ringpropd  14281  ring1  14302  oppr0g  14325  oppr1g  14326  isrhm2d  14410  rhmopp  14421  islring  14437  opprlring  14442  rrgval  14508  isdomn  14516  opprdomnbg  14521  islmod  14565  islmodd  14567  lmodprop2d  14622  lsssetm  14630  islidlm  14753  rnglidlmmgm  14770  rnglidlmsgrp  14771  mplvalcoe  14971  istopg  14990  restbasg  15159  cnfval  15185  cnpfval  15186  txbas  15249  limccl  15650  iswlk  16444  isclwwlk  16515  sscoll2  16884