Theorem rexeqdv 3324

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-rex 3091

This theorem is used by:  rexeqtrdv  3326  rexeqtrrdv  3328  rexeqbidva  3330  fnunirn  7283  oarec  8601  fival  9434  marypha1lem  9455  marypha1  9456  wemapwe  9728  scshwfzeqfzo  15008  supcvg  16057  zprod  16136  vdwlem6  17196  rami  17225  cshws0  17311  imasleval  17745  isssc  18027  fullestrcsetc  18357  fullsetcestrc  18372  ipodrsfi  18745  grppropd  19194  sylow1lem2  19846  sylow3lem1  19874  lsmass  19916  pj1fval  19941  efgrelexlema  19996  pgpfac1lem2  20324  pgpfac1lem3  20326  pgpfac1lem4  20327  dvdsrval  20624  dvdsrpropd  20679  isdrng3lem1  21038  elrspsn  21558  znunit  21902  ellspd  22141  cnpfval  23585  cmpcov  23740  cmpsublem  23750  cmpsub  23751  tgcmp  23752  uncmp  23754  hauscmplem  23757  1stcfb  23796  llyi  23826  nllyi  23827  cldllycmp  23847  ptrescn  23991  isufl  24265  fmid  24312  alexsublem  24396  alexsubb  24398  alexsubALTlem4  24402  alexsubALT  24403  cnextfres1  24420  tsmsf1o  24497  utopval  24584  imasf1oxms  24841  bndth  25312  ovolicc2  25876  ellimc2  26230  limcflf  26234  plyval  26544  aannenlem1  26688  aannenlem2  26689  ulm2  26745  elmade2  28277  tgaaddcpbllem2  29383  brprlng  29449  elntg2  29596  uhgrvtxedgiedgb  29747  nb3grprlem2  29995  cplgrop  30051  cusgrexi  30057  structtocusgr  30060  1egrvtxdg0  30125  erclwwlknsym  30694  erclwwlkntr  30695  hashecclwwlkn1  30701  umgrhashecclwwlk  30702  nfrgr2v  30906  isplig  31111  pjhth  32028  pjhfval  32031  pjhtheu2  32051  lsmssass  34037  0ringirng  34404  iscref  34559  crefeq  34560  issros  34891  eulerpartlemgh  35093  onvf1odlem2  36045  onvf1odlem4  36047  prconf1acwevd  36061  onprcf1of1ord  36068  ispconn  36168  satfv1  36308  satfvsucsuc  36310  br8  36712  br6  36713  br4  36714  wsuclem  36778  brsegle  37064  hilbert1.1  37110  limsucncmpi  37424  pibt2  38545  poimirlem24  38767  poimirlem25  38768  poimirlem27  38770  poimirlem28  38771  volsupnfl  38788  isgrpda  39092  isdrngo2  39095  lcvfbr  40280  pointsetN  41001  dia1dim2  42322  dib1dim2  42428  diclspsn  42454  dih1dimatlem  42589  lcfrvalsnN  42801  mapdpglem3  42935  mapdpglem26  42958  mapdpglem27  42959  prjspnerlem  43849  prjspnnorm  43865  0prjspn  43868  isnacs  43919  eldioph  43973  islssfg  44276  itgoval  44366  uzubioo2  46794  limsupre3uzlem  46960  limsupre3uz  46961  limsupreuz  46962  limsupreuzmpt  46964  liminflelimsuplem  47000  liminflelimsup  47001  liminfreuz  47028  stoweidlem50  47275  stoweidlem57  47282  iccelpart  48730  fargshiftfo  48739  stgrfv  49266  gpgov  49355  lco0  49754  iscnrm3r  50277