Theorem rexeqbidv 2932

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 2924	. 2 |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	rexbidv 2736	. 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 1369   E.wrex 2716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721

This theorem is referenced by:  supeq123d  7700  fpwwe2lem13  8809  vdwpc  14041  ramval  14069  mreexexlemd  14582  iscat  14610  iscatd  14611  catidex  14612  ismnd  15417  mndpropd  15446  gsumval2a  15512  isgrp  15549  isgrpd2e  15560  cayleyth  15920  psgnfval  16006  iscyg  16356  ltbval  17553  opsrval  17556  neiptopnei  18736  is1stc  19045  2ndc1stc  19055  2ndcsep  19063  islly  19072  isnlly  19073  ucnval  19852  imasdsf1olem  19948  met2ndc  20098  evthicc  20943  istrkg2d  22922  legval  23015  nb3graprlem2  23360  isplig  23664  isgrp2d  23722  isgrpda  23784  isexid  23804  isrngo  23865  isrngod  23866  nmoofval  24162  iscvm  27148  cvmlift2lem13  27204  br8  27566  br6  27567  br4  27568  brsegle  28139  hilbert1.1  28185  cover2g  28608  mzpcompact2lem  29088  eldioph  29096  aomclem8  29414  2wlksot  30386  2spthsot  30387  erclwwlkeq  30481  lcoop  30945  ldepsnlinc  31050  lshpset  32623  cvrfval  32913  isatl  32944  ishlat1  32997  llnset  33149  lplnset  33173  lvolset  33216  lineset  33382  lcfl7N  35146  lcfrlem8  35194  lcfrlem9  35195  lcf1o  35196  hvmapffval  35403  hvmapfval  35404  hvmapval  35405