Theorem rexeqdv 3322

Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)

Hypothesis

Ref	Expression
raleqdv.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rexeqdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rexeqdv

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2720  df-rex 3067

This theorem is referenced by:  rexeqbidva  3324  fnunirn  7259  oarec  8577  fival  9430  marypha1lem  9451  marypha1  9452  wemapwe  9715  zornn0g  10523  scshwfzeqfzo  14804  supcvg  15829  zprod  15908  vdwlem6  16949  rami  16978  cshws0  17065  imasleval  17517  isssc  17797  fullestrcsetc  18136  fullsetcestrc  18151  ipodrsfi  18525  grppropd  18902  sylow1lem2  19548  sylow3lem1  19576  lsmass  19618  pj1fval  19643  efgrelexlema  19698  ablfacrplem  20016  pgpfac1lem2  20026  pgpfac1lem3  20028  pgpfac1lem4  20029  ablfac2  20040  dvdsrval  20294  dvdsrpropd  20349  znunit  21491  ellspd  21730  cnpfval  23132  cmpcov  23287  cmpsublem  23297  cmpsub  23298  tgcmp  23299  uncmp  23301  hauscmplem  23304  1stcfb  23343  2ndcctbss  23353  1stcelcls  23359  llyi  23372  nllyi  23373  cldllycmp  23393  ptrescn  23537  isufl  23811  fmid  23858  alexsublem  23942  alexsubb  23944  alexsubALTlem4  23948  alexsubALT  23949  cnextfres1  23966  tsmsf1o  24043  utopval  24131  imasf1oxms  24392  bndth  24878  ovolicc2  25445  ellimc2  25800  limcflf  25804  plyval  26121  aannenlem1  26257  aannenlem2  26258  ulm2  26315  elmade2  27789  elntg2  28790  uhgrvtxedgiedgb  28943  nb3grprlem2  29188  cplgrop  29244  cusgrexi  29250  structtocusgr  29253  1egrvtxdg0  29319  wwlksnextsurj  29705  erclwwlknsym  29874  erclwwlkntr  29875  hashecclwwlkn1  29881  umgrhashecclwwlk  29882  nfrgr2v  30076  isplig  30280  pjhth  31197  pjhfval  31200  pjhtheu2  31220  rspsnel  33078  lsmssass  33106  0ringirng  33358  iscref  33440  crefeq  33441  issros  33789  eulerpartlemgh  33993  ballotlemfc0  34107  ballotlemfcc  34108  ispconn  34828  satfv1  34968  satfvsucsuc  34970  br8  35345  br6  35346  br4  35347  wsuclem  35416  brsegle  35699  hilbert1.1  35745  limsucncmpi  35924  pibt2  36891  poimirlem24  37112  poimirlem25  37113  poimirlem27  37115  poimirlem28  37116  volsupnfl  37133  isgrpda  37423  isdrngo2  37426  lcvfbr  38487  lkrlspeqN  38638  pointsetN  39209  dia1dim2  40530  dib1dim2  40636  diclspsn  40662  dih1dimatlem  40797  lcfrvalsnN  41009  mapdpglem3  41143  mapdpglem26  41166  mapdpglem27  41167  primrootsunit1  41562  prjspnerlem  42032  0prjspn  42043  isnacs  42115  eldioph  42169  islssfg  42485  itgoval  42576  uzubioo2  44945  limsupre3uzlem  45114  limsupre3uz  45115  limsupreuz  45116  limsupreuzmpt  45118  liminflelimsuplem  45154  liminflelimsup  45155  liminfreuz  45182  stoweidlem50  45429  stoweidlem57  45436  iccelpart  46764  fargshiftfo  46773  lco0  47486  iscnrm3r  47958