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

Theorem rexeqdv 3294
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 3288 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067
This theorem is referenced by:  rexeqbidv  3302  rexeqbidva  3304  fnunirn  6653  oarec  7796  fival  8474  marypha1lem  8495  marypha1  8496  wemapwe  8758  zornn0g  9529  scshwfzeqfzo  13777  supcvg  14791  zprod  14870  vdwlem6  15893  rami  15922  cshws0  16011  imasleval  16405  isssc  16683  fullestrcsetc  16995  fullsetcestrc  17010  ipodrsfi  17367  grppropd  17641  sylow1lem2  18217  sylow3lem1  18245  lsmass  18286  pj1fval  18310  efgrelexlema  18365  ablfacrplem  18668  pgpfac1lem2  18678  pgpfac1lem3  18680  pgpfac1lem4  18681  ablfac2  18692  dvdsrval  18849  dvdsrpropd  18900  znunit  20123  ellspd  20354  cnpfval  21255  cmpcov  21409  cmpsublem  21419  cmpsub  21420  tgcmp  21421  uncmp  21423  hauscmplem  21426  1stcfb  21465  2ndcctbss  21475  1stcelcls  21481  llyi  21494  nllyi  21495  cldllycmp  21515  ptrescn  21659  isufl  21933  fmid  21980  alexsublem  22064  alexsubb  22066  alexsubALTlem4  22070  alexsubALT  22071  cnextfres1  22088  tsmsf1o  22164  utopval  22252  imasf1oxms  22510  bndth  22973  ovolicc2  23506  ellimc2  23857  limcflf  23861  plyval  24165  aannenlem1  24299  aannenlem2  24300  ulm2  24355  ishpg  25868  uhgrvtxedgiedgb  26248  uhgrvtxedgiedgbOLD  26249  nb3grprlem2  26502  cplgrop  26564  cusgrexi  26570  structtocusgr  26573  1egrvtxdg0  26638  wwlksnextsur  27040  erclwwlknsym  27224  erclwwlkntr  27225  hashecclwwlkn1  27231  umgrhashecclwwlk  27232  nfrgr2v  27450  isplig  27666  pjhth  28588  pjhfval  28591  pjhtheu2  28611  iscref  30247  crefeq  30248  issros  30574  eulerpartlemgh  30776  ballotlemfc0  30890  ballotlemfcc  30891  ispconn  31539  br8  31980  br6  31981  br4  31982  wsuclem  32103  brsegle  32548  hilbert1.1  32594  limsucncmpi  32777  poimirlem24  33762  poimirlem25  33763  poimirlem27  33765  poimirlem28  33766  volsupnfl  33783  isgrpda  34082  isdrngo2  34085  lcvfbr  34825  lkrlspeqN  34976  pointsetN  35546  dia1dim2  36869  dib1dim2  36975  diclspsn  37001  dih1dimatlem  37136  lcfrvalsnN  37348  mapdpglem3  37482  mapdpglem26  37505  mapdpglem27  37506  isnacs  37790  eldioph  37844  islssfg  38163  itgoval  38254  uzubioo2  40311  limsupre3uzlem  40482  limsupre3uz  40483  limsupreuz  40484  limsupreuzmpt  40486  liminflelimsuplem  40522  liminflelimsup  40523  liminfreuz  40550  stoweidlem50  40781  stoweidlem57  40788  iccelpart  41894  fargshiftfo  41903  lco0  42741
  Copyright terms: Public domain W3C validator