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

Theorem rexeqdv 3175
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 3169 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
31, 2syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947
This theorem is referenced by:  rexeqbidv  3183  rexeqbidva  3185  fnunirn  6551  oarec  7687  fival  8359  marypha1lem  8380  marypha1  8381  wemapwe  8632  zornn0g  9365  scshwfzeqfzo  13618  supcvg  14632  zprod  14711  vdwlem6  15737  rami  15766  cshws0  15855  imasleval  16248  isssc  16527  fullestrcsetc  16838  fullsetcestrc  16853  ipodrsfi  17210  grppropd  17484  sylow1lem2  18060  sylow3lem1  18088  lsmass  18129  pj1fval  18153  efgrelexlema  18208  ablfacrplem  18510  pgpfac1lem2  18520  pgpfac1lem3  18522  pgpfac1lem4  18523  ablfac2  18534  dvdsrval  18691  dvdsrpropd  18742  znunit  19960  ellspd  20189  cnpfval  21086  cmpcov  21240  cmpsublem  21250  cmpsub  21251  tgcmp  21252  uncmp  21254  hauscmplem  21257  1stcfb  21296  2ndcctbss  21306  1stcelcls  21312  llyi  21325  nllyi  21326  cldllycmp  21346  ptrescn  21490  isufl  21764  fmid  21811  alexsublem  21895  alexsubb  21897  alexsubALTlem4  21901  alexsubALT  21902  cnextfres1  21919  tsmsf1o  21995  utopval  22083  imasf1oxms  22341  bndth  22804  ovolicc2  23336  ellimc2  23686  limcflf  23690  plyval  23994  aannenlem1  24128  aannenlem2  24129  ulm2  24184  ishpg  25696  uhgrvtxedgiedgb  26076  nb3grprlem2  26327  cplgrop  26389  cusgrexi  26395  structtocusgr  26398  1egrvtxdg0  26463  wwlksnextsur  26863  erclwwlknsym  27034  erclwwlkntr  27035  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  nfrgr2v  27252  isplig  27458  pjhth  28380  pjhfval  28383  pjhtheu2  28403  iscref  30039  crefeq  30040  issros  30366  eulerpartlemgh  30568  ballotlemfc0  30682  ballotlemfcc  30683  ispconn  31331  br8  31772  br6  31773  br4  31774  wsuclem  31895  brsegle  32340  hilbert1.1  32386  limsucncmpi  32569  poimirlem24  33563  poimirlem25  33564  poimirlem27  33566  poimirlem28  33567  volsupnfl  33584  isgrpda  33884  isdrngo2  33887  lcvfbr  34625  lkrlspeqN  34776  pointsetN  35345  dia1dim2  36668  dib1dim2  36774  diclspsn  36800  dih1dimatlem  36935  lcfrvalsnN  37147  mapdpglem3  37281  mapdpglem26  37304  mapdpglem27  37305  isnacs  37584  eldioph  37638  islssfg  37957  itgoval  38048  uzubioo2  40114  limsupre3uzlem  40285  limsupre3uz  40286  limsupreuz  40287  limsupreuzmpt  40289  liminflelimsuplem  40325  liminflelimsup  40326  liminfreuz  40353  stoweidlem50  40585  stoweidlem57  40592  iccelpart  41694  fargshiftfo  41703  lco0  42541
  Copyright terms: Public domain W3C validator