Theorem rexeqdv 2743

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 2737	. 2 |- ( A = B -> ( E. x e. A ps <-> E. x e. B ps ) )
3	1, 2	syl 15	1 |- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1623   E.wrex 2544

This theorem is referenced by:  rexeqbidv  2749  rexeqbidva  2751  fnunirn  5778  oarec  6560  fival  7166  marypha1lem  7186  marypha1  7187  wemapwe  7400  zornn0g  8132  supcvg  12314  vdwlem6  13033  rami  13062  imasleval  13443  isssc  13697  ipodrsfi  14266  grppropd  14500  sylow1lem2  14910  sylow3lem1  14938  lsmass  14979  pj1fval  15003  efgrelexlema  15058  ablfacrplem  15300  pgpfac1lem2  15310  pgpfac1lem3  15312  pgpfac1lem4  15313  ablfac2  15324  dvdsrval  15427  dvdsrpropd  15478  znunit  16517  cnpfval  16964  cmpcov  17116  cmpsublem  17126  cmpsub  17127  tgcmp  17128  uncmp  17130  hauscmplem  17133  1stcfb  17171  2ndcctbss  17181  1stcelcls  17187  llyi  17200  nllyi  17201  cldllycmp  17221  ptrescn  17333  isufl  17608  fmid  17655  alexsublem  17738  alexsubb  17740  alexsubALTlem4  17744  alexsubALT  17745  tsmsf1o  17827  imasf1oxms  18035  bndth  18456  ovolicc2  18881  ellimc2  19227  limcflf  19231  plyval  19575  aannenlem1  19708  aannenlem2  19709  ulm2  19764  isplig  20844  isgrp2d  20902  isgrpda  20964  pjhth  21972  pjhfval  21975  pjhtheu2  21995  ballotlemfc0  23051  ballotlemfcc  23052  ispcon  23754  br8  24113  br6  24114  br4  24115  brsegle  24731  hilbert1.1  24777  limsucncmpi  24884  fatesg  24956  prjmapcp2  25170  bwt2  25592  bisig0  26062  iscola2  26092  isdrngo2  26589  isnacs  26779  eldioph  26837  islssfg  27168  ellspd  27254  itgoval  27366  frgra2v  28177  lcvfbr  29210  lkrlspeqN  29361  pointsetN  29930  dia1dim2  31252  dib1dim2  31358  diclspsn  31384  dih1dimatlem  31519  lcfrvalsnN  31731  mapdpglem3  31865  mapdpglem26  31888  mapdpglem27  31889

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549