Theorem rexeqdv 3299

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ∃wrex 3064

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 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-rex 3065

This theorem is referenced by:  rexeqtrdv  3301  rexeqtrrdv  3303  rexeqbidva  3305  fnunirn  7204  oarec  8494  fival  9322  marypha1lem  9343  marypha1  9344  wemapwe  9616  scshwfzeqfzo  14786  supcvg  15819  zprod  15900  vdwlem6  16955  rami  16984  cshws0  17070  imasleval  17503  isssc  17785  fullestrcsetc  18115  fullsetcestrc  18130  ipodrsfi  18503  grppropd  18925  sylow1lem2  19572  sylow3lem1  19600  lsmass  19642  pj1fval  19667  efgrelexlema  19722  pgpfac1lem2  20050  pgpfac1lem3  20052  pgpfac1lem4  20053  dvdsrval  20339  dvdsrpropd  20394  elrspsn  21240  znunit  21545  ellspd  21784  cnpfval  23224  cmpcov  23379  cmpsublem  23389  cmpsub  23390  tgcmp  23391  uncmp  23393  hauscmplem  23396  1stcfb  23435  llyi  23464  nllyi  23465  cldllycmp  23485  ptrescn  23629  isufl  23903  fmid  23950  alexsublem  24034  alexsubb  24036  alexsubALTlem4  24040  alexsubALT  24041  cnextfres1  24058  tsmsf1o  24135  utopval  24222  imasf1oxms  24479  bndth  24950  ovolicc2  25514  ellimc2  25869  limcflf  25873  plyval  26183  aannenlem1  26319  aannenlem2  26320  ulm2  26375  elmade2  27875  elntg2  29079  uhgrvtxedgiedgb  29230  nb3grprlem2  29475  cplgrop  29531  cusgrexi  29537  structtocusgr  29540  1egrvtxdg0  29605  erclwwlknsym  30165  erclwwlkntr  30166  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  nfrgr2v  30367  isplig  30572  pjhth  31489  pjhfval  31492  pjhtheu2  31512  lsmssass  33492  0ringirng  33880  iscref  34035  crefeq  34036  issros  34366  eulerpartlemgh  34569  onvf1odlem2  35339  onvf1odlem4  35341  ispconn  35458  satfv1  35598  satfvsucsuc  35600  br8  35991  br6  35992  br4  35993  wsuclem  36058  brsegle  36343  hilbert1.1  36389  limsucncmpi  36680  pibt2  37786  poimirlem24  38018  poimirlem25  38019  poimirlem27  38021  poimirlem28  38022  volsupnfl  38039  isgrpda  38329  isdrngo2  38332  lcvfbr  39519  pointsetN  40240  dia1dim2  41561  dib1dim2  41667  diclspsn  41693  dih1dimatlem  41828  lcfrvalsnN  42040  mapdpglem3  42174  mapdpglem26  42197  mapdpglem27  42198  prjspnerlem  43074  0prjspn  43085  isnacs  43160  eldioph  43214  islssfg  43522  itgoval  43613  uzubioo2  46019  limsupre3uzlem  46185  limsupre3uz  46186  limsupreuz  46187  limsupreuzmpt  46189  liminflelimsuplem  46225  liminflelimsup  46226  liminfreuz  46253  stoweidlem50  46500  stoweidlem57  46507  iccelpart  47915  fargshiftfo  47924  stgrfv  48451  gpgov  48540  lco0  48925  iscnrm3r  49445