Theorem rexeqdv 3325

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-rex 3069

This theorem is referenced by:  rexeqtrdv  3327  rexeqtrrdv  3329  rexeqbidva  3331  fnunirn  7274  oarec  8599  fival  9450  marypha1lem  9471  marypha1  9472  wemapwe  9735  scshwfzeqfzo  14862  supcvg  15889  zprod  15970  vdwlem6  17020  rami  17049  cshws0  17136  imasleval  17588  isssc  17868  fullestrcsetc  18207  fullsetcestrc  18222  ipodrsfi  18597  grppropd  18982  sylow1lem2  19632  sylow3lem1  19660  lsmass  19702  pj1fval  19727  efgrelexlema  19782  pgpfac1lem2  20110  pgpfac1lem3  20112  pgpfac1lem4  20113  dvdsrval  20378  dvdsrpropd  20433  elrspsn  21268  znunit  21600  ellspd  21840  cnpfval  23258  cmpcov  23413  cmpsublem  23423  cmpsub  23424  tgcmp  23425  uncmp  23427  hauscmplem  23430  1stcfb  23469  llyi  23498  nllyi  23499  cldllycmp  23519  ptrescn  23663  isufl  23937  fmid  23984  alexsublem  24068  alexsubb  24070  alexsubALTlem4  24074  alexsubALT  24075  cnextfres1  24092  tsmsf1o  24169  utopval  24257  imasf1oxms  24518  bndth  25004  ovolicc2  25571  ellimc2  25927  limcflf  25931  plyval  26247  aannenlem1  26385  aannenlem2  26386  ulm2  26443  elmade2  27922  elntg2  29015  uhgrvtxedgiedgb  29168  nb3grprlem2  29413  cplgrop  29469  cusgrexi  29475  structtocusgr  29478  1egrvtxdg0  29544  erclwwlknsym  30099  erclwwlkntr  30100  hashecclwwlkn1  30106  umgrhashecclwwlk  30107  nfrgr2v  30301  isplig  30505  pjhth  31422  pjhfval  31425  pjhtheu2  31445  lsmssass  33410  0ringirng  33704  iscref  33805  crefeq  33806  issros  34156  eulerpartlemgh  34360  ispconn  35208  satfv1  35348  satfvsucsuc  35350  br8  35736  br6  35737  br4  35738  wsuclem  35807  brsegle  36090  hilbert1.1  36136  limsucncmpi  36428  pibt2  37400  poimirlem24  37631  poimirlem25  37632  poimirlem27  37634  poimirlem28  37635  volsupnfl  37652  isgrpda  37942  isdrngo2  37945  lcvfbr  39002  pointsetN  39724  dia1dim2  41045  dib1dim2  41151  diclspsn  41177  dih1dimatlem  41312  lcfrvalsnN  41524  mapdpglem3  41658  mapdpglem26  41681  mapdpglem27  41682  prjspnerlem  42604  0prjspn  42615  isnacs  42692  eldioph  42746  islssfg  43059  itgoval  43150  uzubioo2  45522  limsupre3uzlem  45691  limsupre3uz  45692  limsupreuz  45693  limsupreuzmpt  45695  liminflelimsuplem  45731  liminflelimsup  45732  liminfreuz  45759  stoweidlem50  46006  stoweidlem57  46013  iccelpart  47358  fargshiftfo  47367  stgrfv  47856  gpgov  47937  lco0  48273  iscnrm3r  48745