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

Theorem rexeqdv 3121
Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)
Hypothesis
Ref Expression
raleq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
rexeqdv (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rexeqdv
StepHypRef Expression
1 raleq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 rexeq 3115 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901
This theorem is referenced by:  rexeqbidv  3129  rexeqbidva  3131  fnunirn  6392  oarec  7506  fival  8178  marypha1lem  8199  marypha1  8200  wemapwe  8454  zornn0g  9187  scshwfzeqfzo  13371  supcvg  14375  zprod  14454  vdwlem6  15476  rami  15505  cshws0  15594  imasleval  15972  isssc  16251  fullestrcsetc  16562  fullsetcestrc  16577  ipodrsfi  16934  grppropd  17208  sylow1lem2  17785  sylow3lem1  17813  lsmass  17854  pj1fval  17878  efgrelexlema  17933  ablfacrplem  18235  pgpfac1lem2  18245  pgpfac1lem3  18247  pgpfac1lem4  18248  ablfac2  18259  dvdsrval  18416  dvdsrpropd  18467  znunit  19678  ellspd  19907  cnpfval  20795  cmpcov  20949  cmpsublem  20959  cmpsub  20960  tgcmp  20961  uncmp  20963  hauscmplem  20966  1stcfb  21005  2ndcctbss  21015  1stcelcls  21021  llyi  21034  nllyi  21035  cldllycmp  21055  ptrescn  21199  isufl  21474  fmid  21521  alexsublem  21605  alexsubb  21607  alexsubALTlem4  21611  alexsubALT  21612  cnextfres1  21629  tsmsf1o  21705  utopval  21793  imasf1oxms  22051  bndth  22512  ovolicc2  23041  ellimc2  23391  limcflf  23395  plyval  23697  aannenlem1  23831  aannenlem2  23832  ulm2  23887  ishpg  25396  nb3graprlem2  25774  fargshiftfo  25959  wwlkextsur  26052  erclwwlknsym  26147  erclwwlkntr  26148  hashecclwwlkn1  26154  usghashecclwwlk  26155  frgra2v  26319  isplig  26513  pjhth  27429  pjhfval  27432  pjhtheu2  27452  iscref  29032  crefeq  29033  issros  29358  eulerpartlemgh  29560  ballotlemfc0  29674  ballotlemfcc  29675  ispcon  30252  br8  30692  br6  30693  br4  30694  wsuclem  30810  wsuclemOLD  30811  brsegle  31178  hilbert1.1  31224  limsucncmpi  31407  poimirlem24  32386  poimirlem25  32387  poimirlem27  32389  poimirlem28  32390  volsupnfl  32407  isgrpda  32707  isdrngo2  32710  lcvfbr  33108  lkrlspeqN  33259  pointsetN  33828  dia1dim2  35152  dib1dim2  35258  diclspsn  35284  dih1dimatlem  35419  lcfrvalsnN  35631  mapdpglem3  35765  mapdpglem26  35788  mapdpglem27  35789  isnacs  36068  eldioph  36122  islssfg  36441  itgoval  36533  stoweidlem50  38726  stoweidlem57  38733  iccelpart  39755  uhgrvtxedgiedgb  40350  dfnbgr3  40543  nb3grprlem2  40590  cplgrop  40640  cusgrexi  40643  1egrvtxdg0  40708  1wlkvtxedg  40833  wwlksnextsur  41087  erclwwlksnsym  41235  erclwwlksntr  41236  hashecclwwlksn1  41242  umgrhashecclwwlk  41243  nfrgr2v  41423  lco0  41991
  Copyright terms: Public domain W3C validator