Theorem rexeqdv 3326

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ∃wrex 3070

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-rex 3071

This theorem is referenced by:  rexeqbidva  3328  fnunirn  7255  oarec  8564  fival  9409  marypha1lem  9430  marypha1  9431  wemapwe  9694  zornn0g  10502  scshwfzeqfzo  14781  supcvg  15806  zprod  15885  vdwlem6  16923  rami  16952  cshws0  17039  imasleval  17491  isssc  17771  fullestrcsetc  18107  fullsetcestrc  18122  ipodrsfi  18496  grppropd  18873  sylow1lem2  19508  sylow3lem1  19536  lsmass  19578  pj1fval  19603  efgrelexlema  19658  ablfacrplem  19976  pgpfac1lem2  19986  pgpfac1lem3  19988  pgpfac1lem4  19989  ablfac2  20000  dvdsrval  20252  dvdsrpropd  20307  znunit  21338  ellspd  21576  cnpfval  22958  cmpcov  23113  cmpsublem  23123  cmpsub  23124  tgcmp  23125  uncmp  23127  hauscmplem  23130  1stcfb  23169  2ndcctbss  23179  1stcelcls  23185  llyi  23198  nllyi  23199  cldllycmp  23219  ptrescn  23363  isufl  23637  fmid  23684  alexsublem  23768  alexsubb  23770  alexsubALTlem4  23774  alexsubALT  23775  cnextfres1  23792  tsmsf1o  23869  utopval  23957  imasf1oxms  24218  bndth  24698  ovolicc2  25263  ellimc2  25618  limcflf  25622  plyval  25931  aannenlem1  26065  aannenlem2  26066  ulm2  26121  elmade2  27588  elntg2  28498  uhgrvtxedgiedgb  28651  nb3grprlem2  28893  cplgrop  28949  cusgrexi  28955  structtocusgr  28958  1egrvtxdg0  29023  wwlksnextsurj  29409  erclwwlknsym  29578  erclwwlkntr  29579  hashecclwwlkn1  29585  umgrhashecclwwlk  29586  nfrgr2v  29780  isplig  29984  pjhth  30901  pjhfval  30904  pjhtheu2  30924  rspsnel  32746  lsmssass  32774  0ringirng  33030  iscref  33110  crefeq  33111  issros  33459  eulerpartlemgh  33663  ballotlemfc0  33777  ballotlemfcc  33778  ispconn  34500  satfv1  34640  satfvsucsuc  34642  br8  35018  br6  35019  br4  35020  wsuclem  35089  brsegle  35372  hilbert1.1  35418  limsucncmpi  35633  pibt2  36601  poimirlem24  36815  poimirlem25  36816  poimirlem27  36818  poimirlem28  36819  volsupnfl  36836  isgrpda  37126  isdrngo2  37129  lcvfbr  38193  lkrlspeqN  38344  pointsetN  38915  dia1dim2  40236  dib1dim2  40342  diclspsn  40368  dih1dimatlem  40503  lcfrvalsnN  40715  mapdpglem3  40849  mapdpglem26  40872  mapdpglem27  40873  prjspnerlem  41661  0prjspn  41672  isnacs  41744  eldioph  41798  islssfg  42114  itgoval  42205  uzubioo2  44581  limsupre3uzlem  44750  limsupre3uz  44751  limsupreuz  44752  limsupreuzmpt  44754  liminflelimsuplem  44790  liminflelimsup  44791  liminfreuz  44818  stoweidlem50  45065  stoweidlem57  45072  iccelpart  46400  fargshiftfo  46409  lco0  47196  iscnrm3r  47669