Theorem rexeqbidv 2994

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 2986	. 2 |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )
3		raleqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
4	3	rexbidv 2893	. 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 1399   E.wrex 2733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738

This theorem is referenced by:  supeq123d  7824  fpwwe2lem13  8931  vdwpc  14500  ramval  14528  mreexexlemd  15051  iscat  15079  iscatd  15080  catidex  15081  gsumval2a  16023  ismnddef  16039  ismndOLD  16043  mndpropd  16063  isgrp  16178  isgrpd2e  16189  cayleyth  16557  psgnfval  16642  iscyg  16999  ltbval  18249  opsrval  18252  scmatval  19091  pmatcollpw3fi1lem2  19373  pmatcollpw3fi1  19374  neiptopnei  19719  is1stc  20027  2ndc1stc  20037  2ndcsep  20045  islly  20054  isnlly  20055  ucnval  20865  imasdsf1olem  20961  met2ndc  21111  evthicc  21956  istrkg2d  23973  istrkgld  23974  legval  24091  ishpg  24248  iscgra  24289  nb3graprlem2  24573  erclwwlkeq  24932  2wlksot  24988  2spthsot  24989  isplig  25300  isgrp2d  25354  isgrpda  25416  isexid  25436  isrngo  25497  isrngod  25498  nmoofval  25794  iscvm  28893  cvmlift2lem13  28949  br8  29351  br6  29352  br4  29353  brsegle  29911  hilbert1.1  29957  cover2g  30371  mzpcompact2lem  30849  eldioph  30856  aomclem8  31173  zlidlring  32934  uzlidlring  32935  lcoop  33212  ldepsnlinc  33309  nnpw2p  33407  lshpset  35116  cvrfval  35406  isatl  35437  ishlat1  35490  llnset  35642  lplnset  35666  lvolset  35709  lineset  35875  lcfl7N  37641  lcfrlem8  37689  lcfrlem9  37690  lcf1o  37691  hvmapffval  37898  hvmapfval  37899  hvmapval  37900