Theorem rexeqdv 3145

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

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:  rexeqbidv  3153  rexeqbidva  3155  fnunirn  6511  oarec  7642  fival  8318  marypha1lem  8339  marypha1  8340  wemapwe  8594  zornn0g  9327  scshwfzeqfzo  13572  supcvg  14588  zprod  14667  vdwlem6  15690  rami  15719  cshws0  15808  imasleval  16201  isssc  16480  fullestrcsetc  16791  fullsetcestrc  16806  ipodrsfi  17163  grppropd  17437  sylow1lem2  18014  sylow3lem1  18042  lsmass  18083  pj1fval  18107  efgrelexlema  18162  ablfacrplem  18464  pgpfac1lem2  18474  pgpfac1lem3  18476  pgpfac1lem4  18477  ablfac2  18488  dvdsrval  18645  dvdsrpropd  18696  znunit  19912  ellspd  20141  cnpfval  21038  cmpcov  21192  cmpsublem  21202  cmpsub  21203  tgcmp  21204  uncmp  21206  hauscmplem  21209  1stcfb  21248  2ndcctbss  21258  1stcelcls  21264  llyi  21277  nllyi  21278  cldllycmp  21298  ptrescn  21442  isufl  21717  fmid  21764  alexsublem  21848  alexsubb  21850  alexsubALTlem4  21854  alexsubALT  21855  cnextfres1  21872  tsmsf1o  21948  utopval  22036  imasf1oxms  22294  bndth  22757  ovolicc2  23290  ellimc2  23641  limcflf  23645  plyval  23949  aannenlem1  24083  aannenlem2  24084  ulm2  24139  ishpg  25651  uhgrvtxedgiedgb  26031  nb3grprlem2  26283  cplgrop  26333  cusgrexi  26339  structtocusgr  26342  1egrvtxdg0  26407  wwlksnextsur  26795  erclwwlksnsym  26947  erclwwlksntr  26948  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  nfrgr2v  27136  isplig  27328  pjhth  28252  pjhfval  28255  pjhtheu2  28275  iscref  29911  crefeq  29912  issros  30238  eulerpartlemgh  30440  ballotlemfc0  30554  ballotlemfcc  30555  ispconn  31205  br8  31646  br6  31647  br4  31648  wsuclem  31773  wsuclemOLD  31774  brsegle  32215  hilbert1.1  32261  limsucncmpi  32444  poimirlem24  33433  poimirlem25  33434  poimirlem27  33436  poimirlem28  33437  volsupnfl  33454  isgrpda  33754  isdrngo2  33757  lcvfbr  34307  lkrlspeqN  34458  pointsetN  35027  dia1dim2  36351  dib1dim2  36457  diclspsn  36483  dih1dimatlem  36618  lcfrvalsnN  36830  mapdpglem3  36964  mapdpglem26  36987  mapdpglem27  36988  isnacs  37267  eldioph  37321  islssfg  37640  itgoval  37731  uzubioo2  39796  limsupre3uzlem  39967  limsupre3uz  39968  limsupreuz  39969  limsupreuzmpt  39971  liminflelimsuplem  40007  liminflelimsup  40008  liminfreuz  40035  stoweidlem50  40267  stoweidlem57  40274  iccelpart  41369  fargshiftfo  41378  lco0  42216