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 1570  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

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

This theorem is referenced by:  rexeqtrdv  3326  rexeqtrrdv  3328  rexeqbidva  3330  fnunirn  7253  oarec  8548  fival  9373  marypha1lem  9394  marypha1  9395  wemapwe  9667  scshwfzeqfzo  14865  supcvg  15912  zprod  15993  vdwlem6  17047  rami  17076  cshws0  17162  imasleval  17596  isssc  17878  fullestrcsetc  18208  fullsetcestrc  18223  ipodrsfi  18596  grppropd  19019  sylow1lem2  19670  sylow3lem1  19698  lsmass  19740  pj1fval  19765  efgrelexlema  19820  pgpfac1lem2  20148  pgpfac1lem3  20150  pgpfac1lem4  20151  dvdsrval  20444  dvdsrpropd  20499  elrspsn  21352  znunit  21694  ellspd  21933  cnpfval  23372  cmpcov  23527  cmpsublem  23537  cmpsub  23538  tgcmp  23539  uncmp  23541  hauscmplem  23544  1stcfb  23583  llyi  23612  nllyi  23613  cldllycmp  23633  ptrescn  23777  isufl  24051  fmid  24098  alexsublem  24182  alexsubb  24184  alexsubALTlem4  24188  alexsubALT  24189  cnextfres1  24206  tsmsf1o  24283  utopval  24370  imasf1oxms  24627  bndth  25098  ovolicc2  25662  ellimc2  26017  limcflf  26021  plyval  26331  aannenlem1  26472  aannenlem2  26473  ulm2  26529  elmade2  28032  brprlng  29169  elntg2  29316  uhgrvtxedgiedgb  29467  nb3grprlem2  29712  cplgrop  29768  cusgrexi  29774  structtocusgr  29777  1egrvtxdg0  29842  erclwwlknsym  30402  erclwwlkntr  30403  hashecclwwlkn1  30409  umgrhashecclwwlk  30410  nfrgr2v  30604  isplig  30809  pjhth  31726  pjhfval  31729  pjhtheu2  31749  lsmssass  33692  0ringirng  34060  iscref  34215  crefeq  34216  issros  34546  eulerpartlemgh  34749  onvf1odlem2  35569  onvf1odlem4  35571  ispconn  35696  satfv1  35836  satfvsucsuc  35838  br8  36229  br6  36230  br4  36231  wsuclem  36296  brsegle  36581  hilbert1.1  36627  limsucncmpi  36937  pibt2  38044  poimirlem24  38276  poimirlem25  38277  poimirlem27  38279  poimirlem28  38280  volsupnfl  38297  isgrpda  38587  isdrngo2  38590  lcvfbr  39775  pointsetN  40496  dia1dim2  41817  dib1dim2  41923  diclspsn  41949  dih1dimatlem  42084  lcfrvalsnN  42296  mapdpglem3  42430  mapdpglem26  42453  mapdpglem27  42454  prjspnerlem  43332  0prjspn  43343  isnacs  43418  eldioph  43472  islssfg  43780  itgoval  43871  uzubioo2  46266  limsupre3uzlem  46432  limsupre3uz  46433  limsupreuz  46434  limsupreuzmpt  46436  liminflelimsuplem  46472  liminflelimsup  46473  liminfreuz  46500  stoweidlem50  46747  stoweidlem57  46754  iccelpart  48165  fargshiftfo  48174  stgrfv  48701  gpgov  48790  lco0  49190  iscnrm3r  49709