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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-rex 3086

This theorem is referenced by:  rexeqtrdv  3322  rexeqtrrdv  3324  rexeqbidva  3326  fnunirn  7231  oarec  8524  fival  9351  marypha1lem  9372  marypha1  9373  wemapwe  9645  scshwfzeqfzo  14832  supcvg  15876  zprod  15957  vdwlem6  17012  rami  17041  cshws0  17127  imasleval  17561  isssc  17843  fullestrcsetc  18173  fullsetcestrc  18188  ipodrsfi  18561  grppropd  18983  sylow1lem2  19629  sylow3lem1  19657  lsmass  19699  pj1fval  19724  efgrelexlema  19779  pgpfac1lem2  20107  pgpfac1lem3  20109  pgpfac1lem4  20110  dvdsrval  20396  dvdsrpropd  20451  elrspsn  21297  znunit  21602  ellspd  21841  cnpfval  23281  cmpcov  23436  cmpsublem  23446  cmpsub  23447  tgcmp  23448  uncmp  23450  hauscmplem  23453  1stcfb  23492  llyi  23521  nllyi  23522  cldllycmp  23542  ptrescn  23686  isufl  23960  fmid  24007  alexsublem  24091  alexsubb  24093  alexsubALTlem4  24097  alexsubALT  24098  cnextfres1  24115  tsmsf1o  24192  utopval  24279  imasf1oxms  24536  bndth  25007  ovolicc2  25571  ellimc2  25926  limcflf  25930  plyval  26240  aannenlem1  26379  aannenlem2  26380  ulm2  26435  elmade2  27938  elntg2  29142  uhgrvtxedgiedgb  29293  nb3grprlem2  29538  cplgrop  29594  cusgrexi  29600  structtocusgr  29603  1egrvtxdg0  29668  erclwwlknsym  30228  erclwwlkntr  30229  hashecclwwlkn1  30235  umgrhashecclwwlk  30236  nfrgr2v  30430  isplig  30635  pjhth  31552  pjhfval  31555  pjhtheu2  31575  lsmssass  33548  0ringirng  33946  iscref  34101  crefeq  34102  issros  34432  eulerpartlemgh  34635  onvf1odlem2  35407  onvf1odlem4  35409  ispconn  35533  satfv1  35673  satfvsucsuc  35675  br8  36066  br6  36067  br4  36068  wsuclem  36133  brsegle  36418  hilbert1.1  36464  limsucncmpi  36765  pibt2  37871  poimirlem24  38103  poimirlem25  38104  poimirlem27  38106  poimirlem28  38107  volsupnfl  38124  isgrpda  38414  isdrngo2  38417  lcvfbr  39604  pointsetN  40325  dia1dim2  41646  dib1dim2  41752  diclspsn  41778  dih1dimatlem  41913  lcfrvalsnN  42125  mapdpglem3  42259  mapdpglem26  42282  mapdpglem27  42283  prjspnerlem  43159  0prjspn  43170  isnacs  43245  eldioph  43299  islssfg  43607  itgoval  43698  uzubioo2  46103  limsupre3uzlem  46269  limsupre3uz  46270  limsupreuz  46271  limsupreuzmpt  46273  liminflelimsuplem  46309  liminflelimsup  46310  liminfreuz  46337  stoweidlem50  46584  stoweidlem57  46591  iccelpart  47999  fargshiftfo  48008  stgrfv  48535  gpgov  48624  lco0  49009  iscnrm3r  49529