Theorem rexeqdv 3316

Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)

Hypothesis

Ref	Expression
raleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rexeqdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rexeqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rexeq 3310	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1542  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-ral 3058  df-rex 3059

This theorem is referenced by:  rexeqbidva  3322  fnunirn  7017  oarec  8212  fival  8942  marypha1lem  8963  marypha1  8964  wemapwe  9226  zornn0g  9998  scshwfzeqfzo  14270  supcvg  15297  zprod  15376  vdwlem6  16415  rami  16444  cshws0  16531  imasleval  16910  isssc  17188  fullestrcsetc  17510  fullsetcestrc  17525  ipodrsfi  17882  grppropd  18229  sylow1lem2  18835  sylow3lem1  18863  lsmass  18906  pj1fval  18931  efgrelexlema  18986  ablfacrplem  19299  pgpfac1lem2  19309  pgpfac1lem3  19311  pgpfac1lem4  19312  ablfac2  19323  dvdsrval  19510  dvdsrpropd  19561  znunit  20375  ellspd  20611  cnpfval  21978  cmpcov  22133  cmpsublem  22143  cmpsub  22144  tgcmp  22145  uncmp  22147  hauscmplem  22150  1stcfb  22189  2ndcctbss  22199  1stcelcls  22205  llyi  22218  nllyi  22219  cldllycmp  22239  ptrescn  22383  isufl  22657  fmid  22704  alexsublem  22788  alexsubb  22790  alexsubALTlem4  22794  alexsubALT  22795  cnextfres1  22812  tsmsf1o  22889  utopval  22977  imasf1oxms  23235  bndth  23703  ovolicc2  24267  ellimc2  24621  limcflf  24625  plyval  24934  aannenlem1  25068  aannenlem2  25069  ulm2  25124  elntg2  26923  uhgrvtxedgiedgb  27073  nb3grprlem2  27315  cplgrop  27371  cusgrexi  27377  structtocusgr  27380  1egrvtxdg0  27445  wwlksnextsurj  27830  erclwwlknsym  27999  erclwwlkntr  28000  hashecclwwlkn1  28006  umgrhashecclwwlk  28007  nfrgr2v  28201  isplig  28403  pjhth  29320  pjhfval  29323  pjhtheu2  29343  rspsnel  31131  lsmssass  31154  iscref  31358  crefeq  31359  issros  31705  eulerpartlemgh  31907  ballotlemfc0  32021  ballotlemfcc  32022  ispconn  32748  satfv1  32888  satfvsucsuc  32890  br8  33287  br6  33288  br4  33289  wsuclem  33422  elmade2  33681  brsegle  34040  hilbert1.1  34086  limsucncmpi  34264  pibt2  35200  poimirlem24  35413  poimirlem25  35414  poimirlem27  35416  poimirlem28  35417  volsupnfl  35434  isgrpda  35725  isdrngo2  35728  lcvfbr  36646  lkrlspeqN  36797  pointsetN  37367  dia1dim2  38688  dib1dim2  38794  diclspsn  38820  dih1dimatlem  38955  lcfrvalsnN  39167  mapdpglem3  39301  mapdpglem26  39324  mapdpglem27  39325  prjspnerlem  40017  0prjspn  40026  isnacs  40082  eldioph  40136  islssfg  40451  itgoval  40542  uzubioo2  42631  limsupre3uzlem  42802  limsupre3uz  42803  limsupreuz  42804  limsupreuzmpt  42806  liminflelimsuplem  42842  liminflelimsup  42843  liminfreuz  42870  stoweidlem50  43117  stoweidlem57  43124  iccelpart  44403  fargshiftfo  44412  lco0  45286  iscnrm3r  45748