Theorem rexeqdv 3320

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-rex 3087

This theorem is used by:  rexeqtrdv  3322  rexeqtrrdv  3324  rexeqbidva  3326  fnunirn  7258  oarec  8574  fival  9408  marypha1lem  9429  marypha1  9430  wemapwe  9702  scshwfzeqfzo  14982  supcvg  16031  zprod  16110  vdwlem6  17170  rami  17199  cshws0  17285  imasleval  17719  isssc  18001  fullestrcsetc  18331  fullsetcestrc  18346  ipodrsfi  18719  grppropd  19168  sylow1lem2  19819  sylow3lem1  19847  lsmass  19889  pj1fval  19914  efgrelexlema  19969  pgpfac1lem2  20297  pgpfac1lem3  20299  pgpfac1lem4  20300  dvdsrval  20597  dvdsrpropd  20652  isdrng3lem1  21011  elrspsn  21531  znunit  21875  ellspd  22114  cnpfval  23558  cmpcov  23713  cmpsublem  23723  cmpsub  23724  tgcmp  23725  uncmp  23727  hauscmplem  23730  1stcfb  23769  llyi  23799  nllyi  23800  cldllycmp  23820  ptrescn  23964  isufl  24238  fmid  24285  alexsublem  24369  alexsubb  24371  alexsubALTlem4  24375  alexsubALT  24376  cnextfres1  24393  tsmsf1o  24470  utopval  24557  imasf1oxms  24814  bndth  25285  ovolicc2  25849  ellimc2  26203  limcflf  26207  plyval  26517  aannenlem1  26661  aannenlem2  26662  ulm2  26718  elmade2  28250  tgaaddcpbllem2  29356  brprlng  29422  elntg2  29569  uhgrvtxedgiedgb  29720  nb3grprlem2  29968  cplgrop  30024  cusgrexi  30030  structtocusgr  30033  1egrvtxdg0  30098  erclwwlknsym  30667  erclwwlkntr  30668  hashecclwwlkn1  30674  umgrhashecclwwlk  30675  nfrgr2v  30879  isplig  31084  pjhth  32001  pjhfval  32004  pjhtheu2  32024  lsmssass  34000  0ringirng  34368  iscref  34523  crefeq  34524  issros  34855  eulerpartlemgh  35057  onvf1odlem2  35952  onvf1odlem4  35954  prconf1acwevd  35968  onprcf1of1ord  35975  ispconn  36075  satfv1  36215  satfvsucsuc  36217  br8  36614  br6  36615  br4  36616  wsuclem  36680  brsegle  36966  hilbert1.1  37012  limsucncmpi  37326  pibt2  38434  poimirlem24  38656  poimirlem25  38657  poimirlem27  38659  poimirlem28  38660  volsupnfl  38677  isgrpda  38983  isdrngo2  38986  lcvfbr  40171  pointsetN  40892  dia1dim2  42213  dib1dim2  42319  diclspsn  42345  dih1dimatlem  42480  lcfrvalsnN  42692  mapdpglem3  42826  mapdpglem26  42849  mapdpglem27  42850  prjspnerlem  43739  prjspnnorm  43755  0prjspn  43758  isnacs  43809  eldioph  43863  islssfg  44166  itgoval  44257  uzubioo2  46673  limsupre3uzlem  46839  limsupre3uz  46840  limsupreuz  46841  limsupreuzmpt  46843  liminflelimsuplem  46879  liminflelimsup  46880  liminfreuz  46907  stoweidlem50  47154  stoweidlem57  47161  iccelpart  48609  fargshiftfo  48618  stgrfv  49145  gpgov  49234  lco0  49633  iscnrm3r  50156