Theorem rexeqdv 3300

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  rexeqtrdv  3302  rexeqtrrdv  3304  rexeqbidva  3306  fnunirn  7228  oarec  8526  fival  9363  marypha1lem  9384  marypha1  9385  wemapwe  9650  scshwfzeqfzo  14792  supcvg  15822  zprod  15903  vdwlem6  16957  rami  16986  cshws0  17072  imasleval  17504  isssc  17782  fullestrcsetc  18112  fullsetcestrc  18127  ipodrsfi  18498  grppropd  18883  sylow1lem2  19529  sylow3lem1  19557  lsmass  19599  pj1fval  19624  efgrelexlema  19679  pgpfac1lem2  20007  pgpfac1lem3  20009  pgpfac1lem4  20010  dvdsrval  20270  dvdsrpropd  20325  elrspsn  21150  znunit  21473  ellspd  21711  cnpfval  23121  cmpcov  23276  cmpsublem  23286  cmpsub  23287  tgcmp  23288  uncmp  23290  hauscmplem  23293  1stcfb  23332  llyi  23361  nllyi  23362  cldllycmp  23382  ptrescn  23526  isufl  23800  fmid  23847  alexsublem  23931  alexsubb  23933  alexsubALTlem4  23937  alexsubALT  23938  cnextfres1  23955  tsmsf1o  24032  utopval  24120  imasf1oxms  24377  bndth  24857  ovolicc2  25423  ellimc2  25778  limcflf  25782  plyval  26098  aannenlem1  26236  aannenlem2  26237  ulm2  26294  elmade2  27780  elntg2  28912  uhgrvtxedgiedgb  29063  nb3grprlem2  29308  cplgrop  29364  cusgrexi  29370  structtocusgr  29373  1egrvtxdg0  29439  erclwwlknsym  29999  erclwwlkntr  30000  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  nfrgr2v  30201  isplig  30405  pjhth  31322  pjhfval  31325  pjhtheu2  31345  lsmssass  33373  0ringirng  33684  iscref  33834  crefeq  33835  issros  34165  eulerpartlemgh  34369  onvf1odlem2  35091  onvf1odlem4  35093  ispconn  35210  satfv1  35350  satfvsucsuc  35352  br8  35743  br6  35744  br4  35745  wsuclem  35813  brsegle  36096  hilbert1.1  36142  limsucncmpi  36433  pibt2  37405  poimirlem24  37638  poimirlem25  37639  poimirlem27  37641  poimirlem28  37642  volsupnfl  37659  isgrpda  37949  isdrngo2  37952  lcvfbr  39013  pointsetN  39735  dia1dim2  41056  dib1dim2  41162  diclspsn  41188  dih1dimatlem  41323  lcfrvalsnN  41535  mapdpglem3  41669  mapdpglem26  41692  mapdpglem27  41693  prjspnerlem  42605  0prjspn  42616  isnacs  42692  eldioph  42746  islssfg  43059  itgoval  43150  uzubioo2  45565  limsupre3uzlem  45733  limsupre3uz  45734  limsupreuz  45735  limsupreuzmpt  45737  liminflelimsuplem  45773  liminflelimsup  45774  liminfreuz  45801  stoweidlem50  46048  stoweidlem57  46055  iccelpart  47434  fargshiftfo  47443  stgrfv  47952  gpgov  48033  lco0  48416  iscnrm3r  48936