Theorem rexeqdv 3294

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

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

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 2123  ax-ext 2705

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

This theorem is referenced by:  rexeqtrdv  3296  rexeqtrrdv  3298  rexeqbidva  3300  fnunirn  7195  oarec  8485  fival  9305  marypha1lem  9326  marypha1  9327  wemapwe  9596  scshwfzeqfzo  14737  supcvg  15767  zprod  15848  vdwlem6  16902  rami  16931  cshws0  17017  imasleval  17449  isssc  17731  fullestrcsetc  18061  fullsetcestrc  18076  ipodrsfi  18449  grppropd  18868  sylow1lem2  19515  sylow3lem1  19543  lsmass  19585  pj1fval  19610  efgrelexlema  19665  pgpfac1lem2  19993  pgpfac1lem3  19995  pgpfac1lem4  19996  dvdsrval  20283  dvdsrpropd  20338  elrspsn  21181  znunit  21504  ellspd  21743  cnpfval  23152  cmpcov  23307  cmpsublem  23317  cmpsub  23318  tgcmp  23319  uncmp  23321  hauscmplem  23324  1stcfb  23363  llyi  23392  nllyi  23393  cldllycmp  23413  ptrescn  23557  isufl  23831  fmid  23878  alexsublem  23962  alexsubb  23964  alexsubALTlem4  23968  alexsubALT  23969  cnextfres1  23986  tsmsf1o  24063  utopval  24150  imasf1oxms  24407  bndth  24887  ovolicc2  25453  ellimc2  25808  limcflf  25812  plyval  26128  aannenlem1  26266  aannenlem2  26267  ulm2  26324  elmade2  27816  elntg2  28967  uhgrvtxedgiedgb  29118  nb3grprlem2  29363  cplgrop  29419  cusgrexi  29425  structtocusgr  29428  1egrvtxdg0  29494  erclwwlknsym  30054  erclwwlkntr  30055  hashecclwwlkn1  30061  umgrhashecclwwlk  30062  nfrgr2v  30256  isplig  30460  pjhth  31377  pjhfval  31380  pjhtheu2  31400  lsmssass  33376  0ringirng  33725  iscref  33880  crefeq  33881  issros  34211  eulerpartlemgh  34414  onvf1odlem2  35171  onvf1odlem4  35173  ispconn  35290  satfv1  35430  satfvsucsuc  35432  br8  35823  br6  35824  br4  35825  wsuclem  35890  brsegle  36175  hilbert1.1  36221  limsucncmpi  36512  pibt2  37484  poimirlem24  37707  poimirlem25  37708  poimirlem27  37710  poimirlem28  37711  volsupnfl  37728  isgrpda  38018  isdrngo2  38021  lcvfbr  39142  pointsetN  39863  dia1dim2  41184  dib1dim2  41290  diclspsn  41316  dih1dimatlem  41451  lcfrvalsnN  41663  mapdpglem3  41797  mapdpglem26  41820  mapdpglem27  41821  prjspnerlem  42738  0prjspn  42749  isnacs  42824  eldioph  42878  islssfg  43190  itgoval  43281  uzubioo2  45694  limsupre3uzlem  45860  limsupre3uz  45861  limsupreuz  45862  limsupreuzmpt  45864  liminflelimsuplem  45900  liminflelimsup  45901  liminfreuz  45928  stoweidlem50  46175  stoweidlem57  46182  iccelpart  47560  fargshiftfo  47569  stgrfv  48080  gpgov  48169  lco0  48555  iscnrm3r  49075