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

Theorem rexeqdv 3330
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 3324 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wrex 3093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-cleq 2795  df-clel 2798  df-nfc 2933  df-rex 3098
This theorem is referenced by:  rexeqbidv  3338  rexeqbidva  3340  fnunirn  6729  oarec  7873  fival  8551  marypha1lem  8572  marypha1  8573  wemapwe  8835  zornn0g  9606  scshwfzeqfzo  13790  supcvg  14804  zprod  14882  vdwlem6  15901  rami  15930  cshws0  16014  imasleval  16400  isssc  16678  fullestrcsetc  16990  fullsetcestrc  17005  ipodrsfi  17362  grppropd  17636  sylow1lem2  18209  sylow3lem1  18237  lsmass  18278  pj1fval  18302  efgrelexlema  18357  ablfacrplem  18660  pgpfac1lem2  18670  pgpfac1lem3  18672  pgpfac1lem4  18673  ablfac2  18684  dvdsrval  18841  dvdsrpropd  18892  znunit  20113  ellspd  20345  cnpfval  21246  cmpcov  21400  cmpsublem  21410  cmpsub  21411  tgcmp  21412  uncmp  21414  hauscmplem  21417  1stcfb  21456  2ndcctbss  21466  1stcelcls  21472  llyi  21485  nllyi  21486  cldllycmp  21506  ptrescn  21650  isufl  21924  fmid  21971  alexsublem  22055  alexsubb  22057  alexsubALTlem4  22061  alexsubALT  22062  cnextfres1  22079  tsmsf1o  22155  utopval  22243  imasf1oxms  22501  bndth  22964  ovolicc2  23497  ellimc2  23849  limcflf  23853  plyval  24157  aannenlem1  24291  aannenlem2  24292  ulm2  24347  ishpg  25859  uhgrvtxedgiedgb  26239  uhgrvtxedgiedgbOLD  26240  nb3grprlem2  26493  cplgrop  26555  cusgrexi  26561  structtocusgr  26564  1egrvtxdg0  26629  wwlksnextsur  27031  erclwwlknsym  27215  erclwwlkntr  27216  hashecclwwlkn1  27222  umgrhashecclwwlk  27223  nfrgr2v  27441  isplig  27653  pjhth  28574  pjhfval  28577  pjhtheu2  28597  iscref  30230  crefeq  30231  issros  30557  eulerpartlemgh  30759  ballotlemfc0  30873  ballotlemfcc  30874  ispconn  31522  br8  31962  br6  31963  br4  31964  wsuclem  32085  brsegle  32530  hilbert1.1  32576  limsucncmpi  32755  poimirlem24  33740  poimirlem25  33741  poimirlem27  33743  poimirlem28  33744  volsupnfl  33761  isgrpda  34059  isdrngo2  34062  lcvfbr  34794  lkrlspeqN  34945  pointsetN  35515  dia1dim2  36837  dib1dim2  36943  diclspsn  36969  dih1dimatlem  37104  lcfrvalsnN  37316  mapdpglem3  37450  mapdpglem26  37473  mapdpglem27  37474  isnacs  37763  eldioph  37817  islssfg  38135  itgoval  38226  uzubioo2  40270  limsupre3uzlem  40441  limsupre3uz  40442  limsupreuz  40443  limsupreuzmpt  40445  liminflelimsuplem  40481  liminflelimsup  40482  liminfreuz  40509  stoweidlem50  40740  stoweidlem57  40747  iccelpart  41938  fargshiftfo  41947  lco0  42778
  Copyright terms: Public domain W3C validator