Theorem rexeqdv 3296

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-rex 3062

This theorem is referenced by:  rexeqtrdv  3298  rexeqtrrdv  3300  rexeqbidva  3302  fnunirn  7208  oarec  8497  fival  9325  marypha1lem  9346  marypha1  9347  wemapwe  9618  scshwfzeqfzo  14788  supcvg  15821  zprod  15902  vdwlem6  16957  rami  16986  cshws0  17072  imasleval  17505  isssc  17787  fullestrcsetc  18117  fullsetcestrc  18132  ipodrsfi  18505  grppropd  18927  sylow1lem2  19574  sylow3lem1  19602  lsmass  19644  pj1fval  19669  efgrelexlema  19724  pgpfac1lem2  20052  pgpfac1lem3  20054  pgpfac1lem4  20055  dvdsrval  20341  dvdsrpropd  20396  elrspsn  21238  znunit  21543  ellspd  21782  cnpfval  23199  cmpcov  23354  cmpsublem  23364  cmpsub  23365  tgcmp  23366  uncmp  23368  hauscmplem  23371  1stcfb  23410  llyi  23439  nllyi  23440  cldllycmp  23460  ptrescn  23604  isufl  23878  fmid  23925  alexsublem  24009  alexsubb  24011  alexsubALTlem4  24015  alexsubALT  24016  cnextfres1  24033  tsmsf1o  24110  utopval  24197  imasf1oxms  24454  bndth  24925  ovolicc2  25489  ellimc2  25844  limcflf  25848  plyval  26158  aannenlem1  26294  aannenlem2  26295  ulm2  26350  elmade2  27850  elntg2  29054  uhgrvtxedgiedgb  29205  nb3grprlem2  29450  cplgrop  29506  cusgrexi  29512  structtocusgr  29515  1egrvtxdg0  29580  erclwwlknsym  30140  erclwwlkntr  30141  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  nfrgr2v  30342  isplig  30547  pjhth  31464  pjhfval  31467  pjhtheu2  31487  lsmssass  33462  0ringirng  33833  iscref  33988  crefeq  33989  issros  34319  eulerpartlemgh  34522  onvf1odlem2  35286  onvf1odlem4  35288  ispconn  35405  satfv1  35545  satfvsucsuc  35547  br8  35938  br6  35939  br4  35940  wsuclem  36005  brsegle  36290  hilbert1.1  36336  limsucncmpi  36627  pibt2  37733  poimirlem24  37965  poimirlem25  37966  poimirlem27  37968  poimirlem28  37969  volsupnfl  37986  isgrpda  38276  isdrngo2  38279  lcvfbr  39466  pointsetN  40187  dia1dim2  41508  dib1dim2  41614  diclspsn  41640  dih1dimatlem  41775  lcfrvalsnN  41987  mapdpglem3  42121  mapdpglem26  42144  mapdpglem27  42145  prjspnerlem  43050  0prjspn  43061  isnacs  43136  eldioph  43190  islssfg  43498  itgoval  43589  uzubioo2  45997  limsupre3uzlem  46163  limsupre3uz  46164  limsupreuz  46165  limsupreuzmpt  46167  liminflelimsuplem  46203  liminflelimsup  46204  liminfreuz  46231  stoweidlem50  46478  stoweidlem57  46485  iccelpart  47893  fargshiftfo  47902  stgrfv  48429  gpgov  48518  lco0  48903  iscnrm3r  49423