Theorem rexeqbidv 3041

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 3033	. 2 |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	rexbidv 2940	. 2 |- ( ph -> ( E. x e. B ps <-> E. x e. B ch ) )
5	2, 4	bitrd 257	1 |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1438   E.wrex 2777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782

This theorem is referenced by:  supeq123d  7972  fpwwe2lem13  9073  hashge2el2difr  12640  vdwpc  14927  ramval  14957  ramvalOLD  14958  mreexexlemd  15547  iscat  15575  iscatd  15576  catidex  15577  gsumval2a  16519  ismnddef  16535  ismndOLD  16539  mndpropd  16559  isgrp  16674  isgrpd2e  16685  cayleyth  17053  psgnfval  17138  iscyg  17511  ltbval  18692  opsrval  18695  scmatval  19525  pmatcollpw3fi1lem2  19807  pmatcollpw3fi1  19808  neiptopnei  20144  is1stc  20452  2ndc1stc  20462  2ndcsep  20470  islly  20479  isnlly  20480  ucnval  21288  imasdsf1olem  21384  met2ndc  21534  evthicc  22406  istrkgld  24503  legval  24625  ishpg  24797  iscgra  24847  isinag  24875  isleag  24879  nb3graprlem2  25176  erclwwlkeq  25535  2wlksot  25591  2spthsot  25592  isplig  25905  isgrp2d  25959  isgrpda  26021  isexid  26041  isrngo  26102  isrngod  26103  nmoofval  26399  istrkg2d  29489  iscvm  29988  cvmlift2lem13  30044  br8  30401  br6  30402  br4  30403  brsegle  30878  hilbert1.1  30924  poimirlem26  31928  poimirlem28  31930  poimirlem29  31931  cover2g  32003  lshpset  32511  cvrfval  32801  isatl  32832  ishlat1  32885  llnset  33037  lplnset  33061  lvolset  33104  lineset  33270  lcfl7N  35036  lcfrlem8  35084  lcfrlem9  35085  lcf1o  35086  hvmapffval  35293  hvmapfval  35294  hvmapval  35295  mzpcompact2lem  35560  eldioph  35567  aomclem8  35887  ovnval  38185  nnsum3primes4  38643  nnsum3primesprm  38645  nnsum3primesgbe  38647  wtgoldbnnsum4prm  38657  bgoldbnnsum3prm  38659  nbgrval  39023  nb3grprlem2  39051  zlidlring  39320  uzlidlring  39321  lcoop  39598  ldepsnlinc  39695  nnpw2p  39791