Theorem rexeqdv 3306

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-rex 3061

This theorem is referenced by:  rexeqtrdv  3308  rexeqtrrdv  3310  rexeqbidva  3312  fnunirn  7246  oarec  8574  fival  9424  marypha1lem  9445  marypha1  9446  wemapwe  9711  scshwfzeqfzo  14845  supcvg  15872  zprod  15953  vdwlem6  17006  rami  17035  cshws0  17121  imasleval  17555  isssc  17833  fullestrcsetc  18163  fullsetcestrc  18178  ipodrsfi  18549  grppropd  18934  sylow1lem2  19580  sylow3lem1  19608  lsmass  19650  pj1fval  19675  efgrelexlema  19730  pgpfac1lem2  20058  pgpfac1lem3  20060  pgpfac1lem4  20061  dvdsrval  20321  dvdsrpropd  20376  elrspsn  21201  znunit  21524  ellspd  21762  cnpfval  23172  cmpcov  23327  cmpsublem  23337  cmpsub  23338  tgcmp  23339  uncmp  23341  hauscmplem  23344  1stcfb  23383  llyi  23412  nllyi  23413  cldllycmp  23433  ptrescn  23577  isufl  23851  fmid  23898  alexsublem  23982  alexsubb  23984  alexsubALTlem4  23988  alexsubALT  23989  cnextfres1  24006  tsmsf1o  24083  utopval  24171  imasf1oxms  24428  bndth  24908  ovolicc2  25475  ellimc2  25830  limcflf  25834  plyval  26150  aannenlem1  26288  aannenlem2  26289  ulm2  26346  elmade2  27832  elntg2  28964  uhgrvtxedgiedgb  29115  nb3grprlem2  29360  cplgrop  29416  cusgrexi  29422  structtocusgr  29425  1egrvtxdg0  29491  erclwwlknsym  30051  erclwwlkntr  30052  hashecclwwlkn1  30058  umgrhashecclwwlk  30059  nfrgr2v  30253  isplig  30457  pjhth  31374  pjhfval  31377  pjhtheu2  31397  lsmssass  33417  0ringirng  33730  iscref  33875  crefeq  33876  issros  34206  eulerpartlemgh  34410  ispconn  35245  satfv1  35385  satfvsucsuc  35387  br8  35773  br6  35774  br4  35775  wsuclem  35843  brsegle  36126  hilbert1.1  36172  limsucncmpi  36463  pibt2  37435  poimirlem24  37668  poimirlem25  37669  poimirlem27  37671  poimirlem28  37672  volsupnfl  37689  isgrpda  37979  isdrngo2  37982  lcvfbr  39038  pointsetN  39760  dia1dim2  41081  dib1dim2  41187  diclspsn  41213  dih1dimatlem  41348  lcfrvalsnN  41560  mapdpglem3  41694  mapdpglem26  41717  mapdpglem27  41718  prjspnerlem  42640  0prjspn  42651  isnacs  42727  eldioph  42781  islssfg  43094  itgoval  43185  uzubioo2  45596  limsupre3uzlem  45764  limsupre3uz  45765  limsupreuz  45766  limsupreuzmpt  45768  liminflelimsuplem  45804  liminflelimsup  45805  liminfreuz  45832  stoweidlem50  46079  stoweidlem57  46086  iccelpart  47447  fargshiftfo  47456  stgrfv  47965  gpgov  48046  lco0  48403  iscnrm3r  48922