Theorem rexeqbidv 3153

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

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918

This theorem is referenced by:  supeq123d  8356  fpwwe2lem13  9464  hashge2el2difr  13263  vdwpc  15684  ramval  15712  mreexexlemd  16304  iscat  16333  iscatd  16334  catidex  16335  gsumval2a  17279  ismnddef  17296  mndpropd  17316  isgrp  17428  isgrpd2e  17441  cayleyth  17835  psgnfval  17920  iscyg  18281  ltbval  19471  opsrval  19474  scmatval  20310  pmatcollpw3fi1lem2  20592  pmatcollpw3fi1  20593  neiptopnei  20936  is1stc  21244  2ndc1stc  21254  2ndcsep  21262  islly  21271  isnlly  21272  ucnval  22081  imasdsf1olem  22178  met2ndc  22328  evthicc  23228  istrkgld  25358  legval  25479  ishpg  25651  iscgra  25701  isinag  25729  isleag  25733  nbgrval  26234  nb3grprlem2  26283  1loopgrvd0  26400  erclwwlkseq  26932  eucrctshift  27103  isplig  27328  nmoofval  27617  reprsuc  30693  istrkg2d  30744  iscvm  31241  cvmlift2lem13  31297  br8  31646  br6  31647  br4  31648  brsegle  32215  hilbert1.1  32261  poimirlem26  33435  poimirlem28  33437  poimirlem29  33438  cover2g  33509  isexid  33646  isrngo  33696  isrngod  33697  isgrpda  33754  lshpset  34265  cvrfval  34555  isatl  34586  ishlat1  34639  llnset  34791  lplnset  34815  lvolset  34858  lineset  35024  lcfl7N  36790  lcfrlem8  36838  lcfrlem9  36839  lcf1o  36840  hvmapffval  37047  hvmapfval  37048  hvmapval  37049  mzpcompact2lem  37314  eldioph  37321  aomclem8  37631  clsk1independent  38344  ovnval  40755  nnsum3primes4  41676  nnsum3primesprm  41678  nnsum3primesgbe  41680  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  sprval  41729  zlidlring  41928  uzlidlring  41929  lcoop  42200  ldepsnlinc  42297  nnpw2p  42380