Theorem rexeqbidv 3078

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   E.wrex 2818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2823

This theorem is referenced by:  supeq123d  7922  fpwwe2lem13  9032  vdwpc  14374  ramval  14402  mreexexlemd  14916  iscat  14944  iscatd  14945  catidex  14946  gsumval2a  15780  ismnddef  15796  ismndOLD  15799  mndpropd  15819  isgrp  15933  isgrpd2e  15944  cayleyth  16312  psgnfval  16398  iscyg  16755  ltbval  18006  opsrval  18009  scmatval  18875  pmatcollpw3fi1lem2  19157  pmatcollpw3fi1  19158  neiptopnei  19501  is1stc  19810  2ndc1stc  19820  2ndcsep  19828  islly  19837  isnlly  19838  ucnval  20648  imasdsf1olem  20744  met2ndc  20894  evthicc  21739  istrkg2d  23722  istrkgld  23723  legval  23836  nb3graprlem2  24275  erclwwlkeq  24634  2wlksot  24690  2spthsot  24691  isplig  25002  isgrp2d  25060  isgrpda  25122  isexid  25142  isrngo  25203  isrngod  25204  nmoofval  25500  iscvm  28529  cvmlift2lem13  28585  br8  29112  br6  29113  br4  29114  brsegle  29685  hilbert1.1  29731  cover2g  30132  mzpcompact2lem  30612  eldioph  30619  aomclem8  30935  zlidlring  32328  uzlidlring  32329  lcoop  32494  ldepsnlinc  32591  lshpset  34176  cvrfval  34466  isatl  34497  ishlat1  34550  llnset  34702  lplnset  34726  lvolset  34769  lineset  34935  lcfl7N  36699  lcfrlem8  36747  lcfrlem9  36748  lcf1o  36749  hvmapffval  36956  hvmapfval  36957  hvmapval  36958