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 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-rex 3090

This theorem is referenced by:  rexeqtrdv  3326  rexeqtrrdv  3328  rexeqbidva  3330  fnunirn  7241  oarec  8535  fival  9360  marypha1lem  9381  marypha1  9382  wemapwe  9654  scshwfzeqfzo  14851  supcvg  15898  zprod  15979  vdwlem6  17034  rami  17063  cshws0  17149  imasleval  17583  isssc  17865  fullestrcsetc  18195  fullsetcestrc  18210  ipodrsfi  18583  grppropd  19006  sylow1lem2  19657  sylow3lem1  19685  lsmass  19727  pj1fval  19752  efgrelexlema  19807  pgpfac1lem2  20135  pgpfac1lem3  20137  pgpfac1lem4  20138  dvdsrval  20431  dvdsrpropd  20486  elrspsn  21335  znunit  21670  ellspd  21909  cnpfval  23348  cmpcov  23503  cmpsublem  23513  cmpsub  23514  tgcmp  23515  uncmp  23517  hauscmplem  23520  1stcfb  23559  llyi  23588  nllyi  23589  cldllycmp  23609  ptrescn  23753  isufl  24027  fmid  24074  alexsublem  24158  alexsubb  24160  alexsubALTlem4  24164  alexsubALT  24165  cnextfres1  24182  tsmsf1o  24259  utopval  24346  imasf1oxms  24603  bndth  25074  ovolicc2  25638  ellimc2  25993  limcflf  25997  plyval  26307  aannenlem1  26446  aannenlem2  26447  ulm2  26502  elmade2  28005  brprlng  29119  elntg2  29240  uhgrvtxedgiedgb  29391  nb3grprlem2  29636  cplgrop  29692  cusgrexi  29698  structtocusgr  29701  1egrvtxdg0  29766  erclwwlknsym  30326  erclwwlkntr  30327  hashecclwwlkn1  30333  umgrhashecclwwlk  30334  nfrgr2v  30528  isplig  30733  pjhth  31650  pjhfval  31653  pjhtheu2  31673  lsmssass  33622  0ringirng  33991  iscref  34146  crefeq  34147  issros  34477  eulerpartlemgh  34680  onvf1odlem2  35454  onvf1odlem4  35456  ispconn  35581  satfv1  35721  satfvsucsuc  35723  br8  36114  br6  36115  br4  36116  wsuclem  36181  brsegle  36466  hilbert1.1  36512  limsucncmpi  36813  pibt2  37918  poimirlem24  38150  poimirlem25  38151  poimirlem27  38153  poimirlem28  38154  volsupnfl  38171  isgrpda  38461  isdrngo2  38464  lcvfbr  39651  pointsetN  40372  dia1dim2  41693  dib1dim2  41799  diclspsn  41825  dih1dimatlem  41960  lcfrvalsnN  42172  mapdpglem3  42306  mapdpglem26  42329  mapdpglem27  42330  prjspnerlem  43206  0prjspn  43217  isnacs  43292  eldioph  43346  islssfg  43654  itgoval  43745  uzubioo2  46142  limsupre3uzlem  46308  limsupre3uz  46309  limsupreuz  46310  limsupreuzmpt  46312  liminflelimsuplem  46348  liminflelimsup  46349  liminfreuz  46376  stoweidlem50  46623  stoweidlem57  46630  iccelpart  48038  fargshiftfo  48047  stgrfv  48574  gpgov  48663  lco0  49059  iscnrm3r  49578