Theorem rexeqdv 3350

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wrex 3066

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ral 3070  df-rex 3071

This theorem is referenced by:  rexeqbidva  3356  fnunirn  7136  oarec  8402  fival  9180  marypha1lem  9201  marypha1  9202  wemapwe  9464  zornn0g  10270  scshwfzeqfzo  14548  supcvg  15577  zprod  15656  vdwlem6  16696  rami  16725  cshws0  16812  imasleval  17261  isssc  17541  fullestrcsetc  17877  fullsetcestrc  17892  ipodrsfi  18266  grppropd  18603  sylow1lem2  19213  sylow3lem1  19241  lsmass  19284  pj1fval  19309  efgrelexlema  19364  ablfacrplem  19677  pgpfac1lem2  19687  pgpfac1lem3  19689  pgpfac1lem4  19690  ablfac2  19701  dvdsrval  19896  dvdsrpropd  19947  znunit  20780  ellspd  21018  cnpfval  22394  cmpcov  22549  cmpsublem  22559  cmpsub  22560  tgcmp  22561  uncmp  22563  hauscmplem  22566  1stcfb  22605  2ndcctbss  22615  1stcelcls  22621  llyi  22634  nllyi  22635  cldllycmp  22655  ptrescn  22799  isufl  23073  fmid  23120  alexsublem  23204  alexsubb  23206  alexsubALTlem4  23210  alexsubALT  23211  cnextfres1  23228  tsmsf1o  23305  utopval  23393  imasf1oxms  23654  bndth  24130  ovolicc2  24695  ellimc2  25050  limcflf  25054  plyval  25363  aannenlem1  25497  aannenlem2  25498  ulm2  25553  elntg2  27362  uhgrvtxedgiedgb  27515  nb3grprlem2  27757  cplgrop  27813  cusgrexi  27819  structtocusgr  27822  1egrvtxdg0  27887  wwlksnextsurj  28274  erclwwlknsym  28443  erclwwlkntr  28444  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  nfrgr2v  28645  isplig  28847  pjhth  29764  pjhfval  29767  pjhtheu2  29787  rspsnel  31576  lsmssass  31599  iscref  31803  crefeq  31804  issros  32152  eulerpartlemgh  32354  ballotlemfc0  32468  ballotlemfcc  32469  ispconn  33194  satfv1  33334  satfvsucsuc  33336  br8  33732  br6  33733  br4  33734  wsuclem  33828  elmade2  34061  brsegle  34419  hilbert1.1  34465  limsucncmpi  34643  pibt2  35597  poimirlem24  35810  poimirlem25  35811  poimirlem27  35813  poimirlem28  35814  volsupnfl  35831  isgrpda  36122  isdrngo2  36125  lcvfbr  37041  lkrlspeqN  37192  pointsetN  37762  dia1dim2  39083  dib1dim2  39189  diclspsn  39215  dih1dimatlem  39350  lcfrvalsnN  39562  mapdpglem3  39696  mapdpglem26  39719  mapdpglem27  39720  prjspnerlem  40463  0prjspn  40472  isnacs  40533  eldioph  40587  islssfg  40902  itgoval  40993  uzubioo2  43114  limsupre3uzlem  43283  limsupre3uz  43284  limsupreuz  43285  limsupreuzmpt  43287  liminflelimsuplem  43323  liminflelimsup  43324  liminfreuz  43351  stoweidlem50  43598  stoweidlem57  43605  iccelpart  44896  fargshiftfo  44905  lco0  45779  iscnrm3r  46253