Theorem rexeqdv 2875

Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)

Hypothesis

Ref	Expression
raleq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
rexeqdv	|- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hints:   ph( x)   ps( x)

Proof of Theorem rexeqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 |- ( ph -> A = B )
2		rexeq 2869	. 2 |- ( A = B -> ( E. x e. A ps <-> E. x e. B ps ) )
3	1, 2	syl 16	1 |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   E.wrex 2671

This theorem is referenced by:  rexeqbidv  2881  rexeqbidva  2883  fnunirn  5962  oarec  6768  fival  7379  marypha1lem  7400  marypha1  7401  wemapwe  7614  zornn0g  8345  supcvg  12594  vdwlem6  13313  rami  13342  imasleval  13725  isssc  13979  ipodrsfi  14548  grppropd  14782  sylow1lem2  15192  sylow3lem1  15220  lsmass  15261  pj1fval  15285  efgrelexlema  15340  ablfacrplem  15582  pgpfac1lem2  15592  pgpfac1lem3  15594  pgpfac1lem4  15595  ablfac2  15606  dvdsrval  15709  dvdsrpropd  15760  znunit  16803  cnpfval  17256  cmpcov  17410  cmpsublem  17420  cmpsub  17421  tgcmp  17422  uncmp  17424  hauscmplem  17427  1stcfb  17465  2ndcctbss  17475  1stcelcls  17481  llyi  17494  nllyi  17495  cldllycmp  17515  ptrescn  17628  isufl  17902  fmid  17949  alexsublem  18032  alexsubb  18034  alexsubALTlem4  18038  alexsubALT  18039  cnextfres  18056  tsmsf1o  18131  utopval  18219  imasf1oxms  18476  bndth  18940  ovolicc2  19375  ellimc2  19721  limcflf  19725  plyval  20069  aannenlem1  20202  aannenlem2  20203  ulm2  20258  nb3graprlem2  21418  fargshiftfo  21582  isplig  21722  isgrp2d  21780  isgrpda  21842  pjhth  22852  pjhfval  22855  pjhtheu2  22875  ballotlemfc0  24707  ballotlemfcc  24708  ispcon  24867  zprod  25220  br8  25331  br6  25332  br4  25333  brsegle  25950  hilbert1.1  25996  limsucncmpi  26103  volsupnfl  26154  isdrngo2  26468  isnacs  26652  eldioph  26710  islssfg  27040  ellspd  27126  itgoval  27238  stoweidlem50  27670  stoweidlem57  27677  frgra2v  28107  lcvfbr  29507  lkrlspeqN  29658  pointsetN  30227  dia1dim2  31549  dib1dim2  31655  diclspsn  31681  dih1dimatlem  31816  lcfrvalsnN  32028  mapdpglem3  32162  mapdpglem26  32185  mapdpglem27  32186

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2401  df-clel 2404  df-nfc 2533  df-rex 2676