Theorem rexeqdv 3321

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-rex 3088

This theorem is used by:  rexeqtrdv  3323  rexeqtrrdv  3325  rexeqbidva  3327  fnunirn  7249  oarec  8554  fival  9388  marypha1lem  9409  marypha1  9410  wemapwe  9682  scshwfzeqfzo  14957  supcvg  16005  zprod  16084  vdwlem6  17144  rami  17173  cshws0  17259  imasleval  17693  isssc  17975  fullestrcsetc  18305  fullsetcestrc  18320  ipodrsfi  18693  grppropd  19142  sylow1lem2  19793  sylow3lem1  19821  lsmass  19863  pj1fval  19888  efgrelexlema  19943  pgpfac1lem2  20271  pgpfac1lem3  20273  pgpfac1lem4  20274  dvdsrval  20571  dvdsrpropd  20626  isdrng3lem1  20985  elrspsn  21505  znunit  21849  ellspd  22088  cnpfval  23532  cmpcov  23687  cmpsublem  23697  cmpsub  23698  tgcmp  23699  uncmp  23701  hauscmplem  23704  1stcfb  23743  llyi  23773  nllyi  23774  cldllycmp  23794  ptrescn  23938  isufl  24212  fmid  24259  alexsublem  24343  alexsubb  24345  alexsubALTlem4  24349  alexsubALT  24350  cnextfres1  24367  tsmsf1o  24444  utopval  24531  imasf1oxms  24788  bndth  25259  ovolicc2  25823  ellimc2  26177  limcflf  26181  plyval  26491  aannenlem1  26637  aannenlem2  26638  ulm2  26694  elmade2  28226  tgaaddcpbllem2  29332  brprlng  29398  elntg2  29545  uhgrvtxedgiedgb  29696  nb3grprlem2  29944  cplgrop  30000  cusgrexi  30006  structtocusgr  30009  1egrvtxdg0  30074  erclwwlknsym  30643  erclwwlkntr  30644  hashecclwwlkn1  30650  umgrhashecclwwlk  30651  nfrgr2v  30855  isplig  31060  pjhth  31977  pjhfval  31980  pjhtheu2  32000  lsmssass  33935  0ringirng  34303  iscref  34458  crefeq  34459  issros  34790  eulerpartlemgh  34993  onvf1odlem2  35856  onvf1odlem4  35858  ispconn  35957  satfv1  36097  satfvsucsuc  36099  br8  36490  br6  36491  br4  36492  wsuclem  36557  brsegle  36843  hilbert1.1  36889  limsucncmpi  37203  pibt2  38308  poimirlem24  38530  poimirlem25  38531  poimirlem27  38533  poimirlem28  38534  volsupnfl  38551  isgrpda  38857  isdrngo2  38860  lcvfbr  40045  pointsetN  40766  dia1dim2  42087  dib1dim2  42193  diclspsn  42219  dih1dimatlem  42354  lcfrvalsnN  42566  mapdpglem3  42700  mapdpglem26  42723  mapdpglem27  42724  prjspnerlem  43607  0prjspn  43618  isnacs  43668  eldioph  43722  islssfg  44030  itgoval  44121  uzubioo2  46523  limsupre3uzlem  46689  limsupre3uz  46690  limsupreuz  46691  limsupreuzmpt  46693  liminflelimsuplem  46729  liminflelimsup  46730  liminfreuz  46757  stoweidlem50  47004  stoweidlem57  47011  iccelpart  48459  fargshiftfo  48468  stgrfv  48995  gpgov  49084  lco0  49483  iscnrm3r  50000