Theorem rexeqbidv 3014

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
rexeqbidv	|- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )

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

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

Proof of Theorem rexeqbidv

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . 3 |- ( ph -> A = B )
2	1	rexeqdv 3006	. 2 |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	rexbidv 2913	. 2 |- ( ph -> ( E. x e. B ps <-> E. x e. B ch ) )
5	2, 4	bitrd 261	1 |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1455   E.wrex 2750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755

This theorem is referenced by:  supeq123d  7990  fpwwe2lem13  9093  hashge2el2difr  12671  vdwpc  14979  ramval  15009  ramvalOLD  15010  mreexexlemd  15599  iscat  15627  iscatd  15628  catidex  15629  gsumval2a  16571  ismnddef  16587  ismndOLD  16591  mndpropd  16611  isgrp  16726  isgrpd2e  16737  cayleyth  17105  psgnfval  17190  iscyg  17563  ltbval  18744  opsrval  18747  scmatval  19578  pmatcollpw3fi1lem2  19860  pmatcollpw3fi1  19861  neiptopnei  20197  is1stc  20505  2ndc1stc  20515  2ndcsep  20523  islly  20532  isnlly  20533  ucnval  21341  imasdsf1olem  21437  met2ndc  21587  evthicc  22459  istrkgld  24556  legval  24678  ishpg  24850  iscgra  24900  isinag  24928  isleag  24932  nb3graprlem2  25229  erclwwlkeq  25588  2wlksot  25644  2spthsot  25645  isplig  25958  isgrp2d  26012  isgrpda  26074  isexid  26094  isrngo  26155  isrngod  26156  nmoofval  26452  istrkg2d  29532  iscvm  30031  cvmlift2lem13  30087  br8  30445  br6  30446  br4  30447  brsegle  30924  hilbert1.1  30970  poimirlem26  32011  poimirlem28  32013  poimirlem29  32014  cover2g  32086  lshpset  32589  cvrfval  32879  isatl  32910  ishlat1  32963  llnset  33115  lplnset  33139  lvolset  33182  lineset  33348  lcfl7N  35114  lcfrlem8  35162  lcfrlem9  35163  lcf1o  35164  hvmapffval  35371  hvmapfval  35372  hvmapval  35373  mzpcompact2lem  35638  eldioph  35645  aomclem8  35964  ovnval  38400  nnsum3primes4  38921  nnsum3primesprm  38923  nnsum3primesgbe  38925  wtgoldbnnsum4prm  38935  bgoldbnnsum3prm  38937  nbgrval  39456  nb3grprlem2  39505  zlidlring  40201  uzlidlring  40202  lcoop  40477  ldepsnlinc  40574  nnpw2p  40670