Theorem rexeqdv 3122

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

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rexeq 3116	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902

This theorem is referenced by:  rexeqbidv  3130  rexeqbidva  3132  fnunirn  6415  oarec  7529  fival  8201  marypha1lem  8222  marypha1  8223  wemapwe  8477  zornn0g  9210  scshwfzeqfzo  13423  supcvg  14427  zprod  14506  vdwlem6  15528  rami  15557  cshws0  15646  imasleval  16024  isssc  16303  fullestrcsetc  16614  fullsetcestrc  16629  ipodrsfi  16986  grppropd  17260  sylow1lem2  17837  sylow3lem1  17865  lsmass  17906  pj1fval  17930  efgrelexlema  17985  ablfacrplem  18287  pgpfac1lem2  18297  pgpfac1lem3  18299  pgpfac1lem4  18300  ablfac2  18311  dvdsrval  18468  dvdsrpropd  18519  znunit  19731  ellspd  19960  cnpfval  20848  cmpcov  21002  cmpsublem  21012  cmpsub  21013  tgcmp  21014  uncmp  21016  hauscmplem  21019  1stcfb  21058  2ndcctbss  21068  1stcelcls  21074  llyi  21087  nllyi  21088  cldllycmp  21108  ptrescn  21252  isufl  21527  fmid  21574  alexsublem  21658  alexsubb  21660  alexsubALTlem4  21664  alexsubALT  21665  cnextfres1  21682  tsmsf1o  21758  utopval  21846  imasf1oxms  22104  bndth  22565  ovolicc2  23097  ellimc2  23447  limcflf  23451  plyval  23753  aannenlem1  23887  aannenlem2  23888  ulm2  23943  ishpg  25451  uhgrvtxedgiedgb  25810  nb3graprlem2  25981  fargshiftfo  26166  wwlkextsur  26259  erclwwlknsym  26354  erclwwlkntr  26355  hashecclwwlkn1  26361  usghashecclwwlk  26362  frgra2v  26526  isplig  26720  pjhth  27636  pjhfval  27639  pjhtheu2  27659  iscref  29239  crefeq  29240  issros  29565  eulerpartlemgh  29767  ballotlemfc0  29881  ballotlemfcc  29882  ispcon  30459  br8  30899  br6  30900  br4  30901  wsuclem  31017  wsuclemOLD  31018  brsegle  31385  hilbert1.1  31431  limsucncmpi  31614  poimirlem24  32603  poimirlem25  32604  poimirlem27  32606  poimirlem28  32607  volsupnfl  32624  isgrpda  32924  isdrngo2  32927  lcvfbr  33325  lkrlspeqN  33476  pointsetN  34045  dia1dim2  35369  dib1dim2  35475  diclspsn  35501  dih1dimatlem  35636  lcfrvalsnN  35848  mapdpglem3  35982  mapdpglem26  36005  mapdpglem27  36006  isnacs  36285  eldioph  36339  islssfg  36658  itgoval  36750  stoweidlem50  38943  stoweidlem57  38950  iccelpart  39971  dfnbgr3  40562  nb3grprlem2  40609  cplgrop  40659  cusgrexi  40662  1egrvtxdg0  40727  1wlkvtxedg  40852  wwlksnextsur  41106  erclwwlksnsym  41254  erclwwlksntr  41255  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  nfrgr2v  41442  lco0  42010