Theorem rexeqdv 3327

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

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

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 2708

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

This theorem is referenced by:  rexeqtrdv  3329  rexeqtrrdv  3331  rexeqbidva  3333  fnunirn  7274  oarec  8600  fival  9452  marypha1lem  9473  marypha1  9474  wemapwe  9737  scshwfzeqfzo  14865  supcvg  15892  zprod  15973  vdwlem6  17024  rami  17053  cshws0  17139  imasleval  17586  isssc  17864  fullestrcsetc  18196  fullsetcestrc  18211  ipodrsfi  18584  grppropd  18969  sylow1lem2  19617  sylow3lem1  19645  lsmass  19687  pj1fval  19712  efgrelexlema  19767  pgpfac1lem2  20095  pgpfac1lem3  20097  pgpfac1lem4  20098  dvdsrval  20361  dvdsrpropd  20416  elrspsn  21250  znunit  21582  ellspd  21822  cnpfval  23242  cmpcov  23397  cmpsublem  23407  cmpsub  23408  tgcmp  23409  uncmp  23411  hauscmplem  23414  1stcfb  23453  llyi  23482  nllyi  23483  cldllycmp  23503  ptrescn  23647  isufl  23921  fmid  23968  alexsublem  24052  alexsubb  24054  alexsubALTlem4  24058  alexsubALT  24059  cnextfres1  24076  tsmsf1o  24153  utopval  24241  imasf1oxms  24502  bndth  24990  ovolicc2  25557  ellimc2  25912  limcflf  25916  plyval  26232  aannenlem1  26370  aannenlem2  26371  ulm2  26428  elmade2  27907  elntg2  29000  uhgrvtxedgiedgb  29153  nb3grprlem2  29398  cplgrop  29454  cusgrexi  29460  structtocusgr  29463  1egrvtxdg0  29529  erclwwlknsym  30089  erclwwlkntr  30090  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  nfrgr2v  30291  isplig  30495  pjhth  31412  pjhfval  31415  pjhtheu2  31435  lsmssass  33430  0ringirng  33739  iscref  33843  crefeq  33844  issros  34176  eulerpartlemgh  34380  ispconn  35228  satfv1  35368  satfvsucsuc  35370  br8  35756  br6  35757  br4  35758  wsuclem  35826  brsegle  36109  hilbert1.1  36155  limsucncmpi  36446  pibt2  37418  poimirlem24  37651  poimirlem25  37652  poimirlem27  37654  poimirlem28  37655  volsupnfl  37672  isgrpda  37962  isdrngo2  37965  lcvfbr  39021  pointsetN  39743  dia1dim2  41064  dib1dim2  41170  diclspsn  41196  dih1dimatlem  41331  lcfrvalsnN  41543  mapdpglem3  41677  mapdpglem26  41700  mapdpglem27  41701  prjspnerlem  42627  0prjspn  42638  isnacs  42715  eldioph  42769  islssfg  43082  itgoval  43173  uzubioo2  45582  limsupre3uzlem  45750  limsupre3uz  45751  limsupreuz  45752  limsupreuzmpt  45754  liminflelimsuplem  45790  liminflelimsup  45791  liminfreuz  45818  stoweidlem50  46065  stoweidlem57  46072  iccelpart  47420  fargshiftfo  47429  stgrfv  47920  gpgov  48001  lco0  48344  iscnrm3r  48845