Theorem rexeqdv 3297

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 3292	. 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  3299  rexeqtrrdv  3301  rexeqbidva  3303  fnunirn  7201  oarec  8490  fival  9318  marypha1lem  9339  marypha1  9340  wemapwe  9609  scshwfzeqfzo  14779  supcvg  15812  zprod  15893  vdwlem6  16948  rami  16977  cshws0  17063  imasleval  17496  isssc  17778  fullestrcsetc  18108  fullsetcestrc  18123  ipodrsfi  18496  grppropd  18918  sylow1lem2  19565  sylow3lem1  19593  lsmass  19635  pj1fval  19660  efgrelexlema  19715  pgpfac1lem2  20043  pgpfac1lem3  20045  pgpfac1lem4  20046  dvdsrval  20332  dvdsrpropd  20387  elrspsn  21230  znunit  21553  ellspd  21792  cnpfval  23209  cmpcov  23364  cmpsublem  23374  cmpsub  23375  tgcmp  23376  uncmp  23378  hauscmplem  23381  1stcfb  23420  llyi  23449  nllyi  23450  cldllycmp  23470  ptrescn  23614  isufl  23888  fmid  23935  alexsublem  24019  alexsubb  24021  alexsubALTlem4  24025  alexsubALT  24026  cnextfres1  24043  tsmsf1o  24120  utopval  24207  imasf1oxms  24464  bndth  24935  ovolicc2  25499  ellimc2  25854  limcflf  25858  plyval  26168  aannenlem1  26305  aannenlem2  26306  ulm2  26363  elmade2  27864  elntg2  29068  uhgrvtxedgiedgb  29219  nb3grprlem2  29464  cplgrop  29520  cusgrexi  29526  structtocusgr  29529  1egrvtxdg0  29595  erclwwlknsym  30155  erclwwlkntr  30156  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  nfrgr2v  30357  isplig  30562  pjhth  31479  pjhfval  31482  pjhtheu2  31502  lsmssass  33477  0ringirng  33849  iscref  34004  crefeq  34005  issros  34335  eulerpartlemgh  34538  onvf1odlem2  35302  onvf1odlem4  35304  ispconn  35421  satfv1  35561  satfvsucsuc  35563  br8  35954  br6  35955  br4  35956  wsuclem  36021  brsegle  36306  hilbert1.1  36352  limsucncmpi  36643  pibt2  37747  poimirlem24  37979  poimirlem25  37980  poimirlem27  37982  poimirlem28  37983  volsupnfl  38000  isgrpda  38290  isdrngo2  38293  lcvfbr  39480  pointsetN  40201  dia1dim2  41522  dib1dim2  41628  diclspsn  41654  dih1dimatlem  41789  lcfrvalsnN  42001  mapdpglem3  42135  mapdpglem26  42158  mapdpglem27  42159  prjspnerlem  43064  0prjspn  43075  isnacs  43150  eldioph  43204  islssfg  43516  itgoval  43607  uzubioo2  46015  limsupre3uzlem  46181  limsupre3uz  46182  limsupreuz  46183  limsupreuzmpt  46185  liminflelimsuplem  46221  liminflelimsup  46222  liminfreuz  46249  stoweidlem50  46496  stoweidlem57  46503  iccelpart  47905  fargshiftfo  47914  stgrfv  48441  gpgov  48530  lco0  48915  iscnrm3r  49435