Theorem rexeqdv 3327

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-rex 3072

This theorem is referenced by:  rexeqbidva  3329  fnunirn  7253  oarec  8562  fival  9407  marypha1lem  9428  marypha1  9429  wemapwe  9692  zornn0g  10500  scshwfzeqfzo  14777  supcvg  15802  zprod  15881  vdwlem6  16919  rami  16948  cshws0  17035  imasleval  17487  isssc  17767  fullestrcsetc  18103  fullsetcestrc  18118  ipodrsfi  18492  grppropd  18837  sylow1lem2  19467  sylow3lem1  19495  lsmass  19537  pj1fval  19562  efgrelexlema  19617  ablfacrplem  19935  pgpfac1lem2  19945  pgpfac1lem3  19947  pgpfac1lem4  19948  ablfac2  19959  dvdsrval  20175  dvdsrpropd  20230  znunit  21119  ellspd  21357  cnpfval  22738  cmpcov  22893  cmpsublem  22903  cmpsub  22904  tgcmp  22905  uncmp  22907  hauscmplem  22910  1stcfb  22949  2ndcctbss  22959  1stcelcls  22965  llyi  22978  nllyi  22979  cldllycmp  22999  ptrescn  23143  isufl  23417  fmid  23464  alexsublem  23548  alexsubb  23550  alexsubALTlem4  23554  alexsubALT  23555  cnextfres1  23572  tsmsf1o  23649  utopval  23737  imasf1oxms  23998  bndth  24474  ovolicc2  25039  ellimc2  25394  limcflf  25398  plyval  25707  aannenlem1  25841  aannenlem2  25842  ulm2  25897  elmade2  27364  elntg2  28274  uhgrvtxedgiedgb  28427  nb3grprlem2  28669  cplgrop  28725  cusgrexi  28731  structtocusgr  28734  1egrvtxdg0  28799  wwlksnextsurj  29185  erclwwlknsym  29354  erclwwlkntr  29355  hashecclwwlkn1  29361  umgrhashecclwwlk  29362  nfrgr2v  29556  isplig  29760  pjhth  30677  pjhfval  30680  pjhtheu2  30700  rspsnel  32515  lsmssass  32543  0ringirng  32784  iscref  32855  crefeq  32856  issros  33204  eulerpartlemgh  33408  ballotlemfc0  33522  ballotlemfcc  33523  ispconn  34245  satfv1  34385  satfvsucsuc  34387  br8  34757  br6  34758  br4  34759  wsuclem  34828  brsegle  35111  hilbert1.1  35157  limsucncmpi  35378  pibt2  36346  poimirlem24  36560  poimirlem25  36561  poimirlem27  36563  poimirlem28  36564  volsupnfl  36581  isgrpda  36871  isdrngo2  36874  lcvfbr  37938  lkrlspeqN  38089  pointsetN  38660  dia1dim2  39981  dib1dim2  40087  diclspsn  40113  dih1dimatlem  40248  lcfrvalsnN  40460  mapdpglem3  40594  mapdpglem26  40617  mapdpglem27  40618  prjspnerlem  41407  0prjspn  41418  isnacs  41490  eldioph  41544  islssfg  41860  itgoval  41951  uzubioo2  44330  limsupre3uzlem  44499  limsupre3uz  44500  limsupreuz  44501  limsupreuzmpt  44503  liminflelimsuplem  44539  liminflelimsup  44540  liminfreuz  44567  stoweidlem50  44814  stoweidlem57  44821  iccelpart  46149  fargshiftfo  46158  lco0  47156  iscnrm3r  47629