Theorem rexeqdv 3321

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  rexeqtrdv  3323  rexeqtrrdv  3325  rexeqbidva  3327  fnunirn  7257  oarec  8570  fival  9404  marypha1lem  9425  marypha1  9426  wemapwe  9698  scshwfzeqfzo  14977  supcvg  16025  zprod  16104  vdwlem6  17164  rami  17193  cshws0  17279  imasleval  17713  isssc  17995  fullestrcsetc  18325  fullsetcestrc  18340  ipodrsfi  18713  grppropd  19162  sylow1lem2  19813  sylow3lem1  19841  lsmass  19883  pj1fval  19908  efgrelexlema  19963  pgpfac1lem2  20291  pgpfac1lem3  20293  pgpfac1lem4  20294  dvdsrval  20591  dvdsrpropd  20646  isdrng3lem1  21005  elrspsn  21525  znunit  21869  ellspd  22108  cnpfval  23552  cmpcov  23707  cmpsublem  23717  cmpsub  23718  tgcmp  23719  uncmp  23721  hauscmplem  23724  1stcfb  23763  llyi  23793  nllyi  23794  cldllycmp  23814  ptrescn  23958  isufl  24232  fmid  24279  alexsublem  24363  alexsubb  24365  alexsubALTlem4  24369  alexsubALT  24370  cnextfres1  24387  tsmsf1o  24464  utopval  24551  imasf1oxms  24808  bndth  25279  ovolicc2  25843  ellimc2  26197  limcflf  26201  plyval  26511  aannenlem1  26655  aannenlem2  26656  ulm2  26712  elmade2  28244  tgaaddcpbllem2  29350  brprlng  29416  elntg2  29563  uhgrvtxedgiedgb  29714  nb3grprlem2  29962  cplgrop  30018  cusgrexi  30024  structtocusgr  30027  1egrvtxdg0  30092  erclwwlknsym  30661  erclwwlkntr  30662  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  nfrgr2v  30873  isplig  31078  pjhth  31995  pjhfval  31998  pjhtheu2  32018  lsmssass  33953  0ringirng  34321  iscref  34476  crefeq  34477  issros  34808  eulerpartlemgh  35010  onvf1odlem2  35883  onvf1odlem4  35885  ispconn  35988  satfv1  36128  satfvsucsuc  36130  br8  36521  br6  36522  br4  36523  wsuclem  36587  brsegle  36873  hilbert1.1  36919  limsucncmpi  37233  pibt2  38340  poimirlem24  38562  poimirlem25  38563  poimirlem27  38565  poimirlem28  38566  volsupnfl  38583  isgrpda  38889  isdrngo2  38892  lcvfbr  40077  pointsetN  40798  dia1dim2  42119  dib1dim2  42225  diclspsn  42251  dih1dimatlem  42386  lcfrvalsnN  42598  mapdpglem3  42732  mapdpglem26  42755  mapdpglem27  42756  prjspnerlem  43645  prjspnnorm  43661  0prjspn  43664  isnacs  43714  eldioph  43768  islssfg  44071  itgoval  44162  uzubioo2  46578  limsupre3uzlem  46744  limsupre3uz  46745  limsupreuz  46746  limsupreuzmpt  46748  liminflelimsuplem  46784  liminflelimsup  46785  liminfreuz  46812  stoweidlem50  47059  stoweidlem57  47066  iccelpart  48514  fargshiftfo  48523  stgrfv  49050  gpgov  49139  lco0  49538  iscnrm3r  50055