Theorem rexeqdv 3293

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-rex 3057

This theorem is referenced by:  rexeqtrdv  3295  rexeqtrrdv  3297  rexeqbidva  3299  fnunirn  7187  oarec  8477  fival  9296  marypha1lem  9317  marypha1  9318  wemapwe  9587  scshwfzeqfzo  14733  supcvg  15763  zprod  15844  vdwlem6  16898  rami  16927  cshws0  17013  imasleval  17445  isssc  17727  fullestrcsetc  18057  fullsetcestrc  18072  ipodrsfi  18445  grppropd  18864  sylow1lem2  19512  sylow3lem1  19540  lsmass  19582  pj1fval  19607  efgrelexlema  19662  pgpfac1lem2  19990  pgpfac1lem3  19992  pgpfac1lem4  19993  dvdsrval  20280  dvdsrpropd  20335  elrspsn  21178  znunit  21501  ellspd  21740  cnpfval  23150  cmpcov  23305  cmpsublem  23315  cmpsub  23316  tgcmp  23317  uncmp  23319  hauscmplem  23322  1stcfb  23361  llyi  23390  nllyi  23391  cldllycmp  23411  ptrescn  23555  isufl  23829  fmid  23876  alexsublem  23960  alexsubb  23962  alexsubALTlem4  23966  alexsubALT  23967  cnextfres1  23984  tsmsf1o  24061  utopval  24148  imasf1oxms  24405  bndth  24885  ovolicc2  25451  ellimc2  25806  limcflf  25810  plyval  26126  aannenlem1  26264  aannenlem2  26265  ulm2  26322  elmade2  27814  elntg2  28964  uhgrvtxedgiedgb  29115  nb3grprlem2  29360  cplgrop  29416  cusgrexi  29422  structtocusgr  29425  1egrvtxdg0  29491  erclwwlknsym  30048  erclwwlkntr  30049  hashecclwwlkn1  30055  umgrhashecclwwlk  30056  nfrgr2v  30250  isplig  30454  pjhth  31371  pjhfval  31374  pjhtheu2  31394  lsmssass  33365  0ringirng  33700  iscref  33855  crefeq  33856  issros  34186  eulerpartlemgh  34389  onvf1odlem2  35146  onvf1odlem4  35148  ispconn  35265  satfv1  35405  satfvsucsuc  35407  br8  35798  br6  35799  br4  35800  wsuclem  35865  brsegle  36148  hilbert1.1  36194  limsucncmpi  36485  pibt2  37457  poimirlem24  37690  poimirlem25  37691  poimirlem27  37693  poimirlem28  37694  volsupnfl  37711  isgrpda  38001  isdrngo2  38004  lcvfbr  39065  pointsetN  39786  dia1dim2  41107  dib1dim2  41213  diclspsn  41239  dih1dimatlem  41374  lcfrvalsnN  41586  mapdpglem3  41720  mapdpglem26  41743  mapdpglem27  41744  prjspnerlem  42656  0prjspn  42667  isnacs  42743  eldioph  42797  islssfg  43109  itgoval  43200  uzubioo2  45613  limsupre3uzlem  45779  limsupre3uz  45780  limsupreuz  45781  limsupreuzmpt  45783  liminflelimsuplem  45819  liminflelimsup  45820  liminfreuz  45847  stoweidlem50  46094  stoweidlem57  46101  iccelpart  47470  fargshiftfo  47479  stgrfv  47990  gpgov  48079  lco0  48465  iscnrm3r  48985