Theorem rexeqdv 3299

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 3294	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-rex 3063

This theorem is referenced by:  rexeqtrdv  3301  rexeqtrrdv  3303  rexeqbidva  3305  fnunirn  7209  oarec  8499  fival  9327  marypha1lem  9348  marypha1  9349  wemapwe  9618  scshwfzeqfzo  14761  supcvg  15791  zprod  15872  vdwlem6  16926  rami  16955  cshws0  17041  imasleval  17474  isssc  17756  fullestrcsetc  18086  fullsetcestrc  18101  ipodrsfi  18474  grppropd  18893  sylow1lem2  19540  sylow3lem1  19568  lsmass  19610  pj1fval  19635  efgrelexlema  19690  pgpfac1lem2  20018  pgpfac1lem3  20020  pgpfac1lem4  20021  dvdsrval  20309  dvdsrpropd  20364  elrspsn  21207  znunit  21530  ellspd  21769  cnpfval  23190  cmpcov  23345  cmpsublem  23355  cmpsub  23356  tgcmp  23357  uncmp  23359  hauscmplem  23362  1stcfb  23401  llyi  23430  nllyi  23431  cldllycmp  23451  ptrescn  23595  isufl  23869  fmid  23916  alexsublem  24000  alexsubb  24002  alexsubALTlem4  24006  alexsubALT  24007  cnextfres1  24024  tsmsf1o  24101  utopval  24188  imasf1oxms  24445  bndth  24925  ovolicc2  25491  ellimc2  25846  limcflf  25850  plyval  26166  aannenlem1  26304  aannenlem2  26305  ulm2  26362  elmade2  27866  elntg2  29070  uhgrvtxedgiedgb  29221  nb3grprlem2  29466  cplgrop  29522  cusgrexi  29528  structtocusgr  29531  1egrvtxdg0  29597  erclwwlknsym  30157  erclwwlkntr  30158  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  nfrgr2v  30359  isplig  30563  pjhth  31480  pjhfval  31483  pjhtheu2  31503  lsmssass  33494  0ringirng  33866  iscref  34021  crefeq  34022  issros  34352  eulerpartlemgh  34555  onvf1odlem2  35317  onvf1odlem4  35319  ispconn  35436  satfv1  35576  satfvsucsuc  35578  br8  35969  br6  35970  br4  35971  wsuclem  36036  brsegle  36321  hilbert1.1  36367  limsucncmpi  36658  pibt2  37669  poimirlem24  37892  poimirlem25  37893  poimirlem27  37895  poimirlem28  37896  volsupnfl  37913  isgrpda  38203  isdrngo2  38206  lcvfbr  39393  pointsetN  40114  dia1dim2  41435  dib1dim2  41541  diclspsn  41567  dih1dimatlem  41702  lcfrvalsnN  41914  mapdpglem3  42048  mapdpglem26  42071  mapdpglem27  42072  prjspnerlem  42972  0prjspn  42983  isnacs  43058  eldioph  43112  islssfg  43424  itgoval  43515  uzubioo2  45924  limsupre3uzlem  46090  limsupre3uz  46091  limsupreuz  46092  limsupreuzmpt  46094  liminflelimsuplem  46130  liminflelimsup  46131  liminfreuz  46158  stoweidlem50  46405  stoweidlem57  46412  iccelpart  47790  fargshiftfo  47799  stgrfv  48310  gpgov  48399  lco0  48784  iscnrm3r  49304