MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexeqdv Structured version   Unicode version

Theorem rexeqdv 2914
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
StepHypRef Expression
1 raleq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 rexeq 2908 . 2  |-  ( A  =  B  ->  ( E. x  e.  A  ps 
<->  E. x  e.  B  ps ) )
31, 2syl 16 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711
This theorem is referenced by:  rexeqbidv  2922  rexeqbidva  2924  fnunirn  5956  oarec  6989  fival  7650  marypha1lem  7671  marypha1  7672  wemapwe  7916  wemapweOLD  7917  zornn0g  8662  supcvg  13300  vdwlem6  14029  rami  14058  cshws0  14110  imasleval  14461  isssc  14715  ipodrsfi  15315  grppropd  15535  sylow1lem2  16077  sylow3lem1  16105  lsmass  16146  pj1fval  16170  efgrelexlema  16225  ablfacrplem  16539  pgpfac1lem2  16549  pgpfac1lem3  16551  pgpfac1lem4  16552  ablfac2  16563  dvdsrval  16670  dvdsrpropd  16721  znunit  17837  ellspd  18071  ellspdOLD  18072  cnpfval  18679  cmpcov  18833  cmpsublem  18843  cmpsub  18844  tgcmp  18845  uncmp  18847  hauscmplem  18850  bwthOLD  18855  1stcfb  18890  2ndcctbss  18900  1stcelcls  18906  llyi  18919  nllyi  18920  cldllycmp  18940  ptrescn  19053  isufl  19327  fmid  19374  alexsublem  19457  alexsubb  19459  alexsubALTlem4  19463  alexsubALT  19464  cnextfres  19481  tsmsf1o  19560  utopval  19648  imasf1oxms  19905  bndth  20371  ovolicc2  20846  ellimc2  21193  limcflf  21197  plyval  21545  aannenlem1  21678  aannenlem2  21679  ulm2  21734  nb3graprlem2  23182  fargshiftfo  23346  isplig  23486  isgrp2d  23544  isgrpda  23606  pjhth  24618  pjhfval  24621  pjhtheu2  24641  eulerpartlemgh  26608  ballotlemfc0  26722  ballotlemfcc  26723  ispcon  26959  zprod  27296  br8  27412  br6  27413  br4  27414  wsuclem  27608  brsegle  27985  hilbert1.1  28031  limsucncmpi  28138  volsupnfl  28277  isdrngo2  28605  isnacs  28882  eldioph  28938  islssfg  29265  itgoval  29360  stoweidlem50  29688  stoweidlem57  29695  wwlkextsur  30206  scshwfzeqfzo  30335  erclwwlknsym  30343  erclwwlkntr  30344  hashecclwwlkn1  30351  usghashecclwwlk  30352  frgra2v  30434  lco0  30667  lcvfbr  32235  lkrlspeqN  32386  pointsetN  32955  dia1dim2  34277  dib1dim2  34383  diclspsn  34409  dih1dimatlem  34544  lcfrvalsnN  34756  mapdpglem3  34890  mapdpglem26  34913  mapdpglem27  34914
  Copyright terms: Public domain W3C validator