Theorem rexeqdv 3325

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-rex 3070

This theorem is referenced by:  rexeqbidva  3327  fnunirn  7256  oarec  8568  fival  9413  marypha1lem  9434  marypha1  9435  wemapwe  9698  zornn0g  10506  scshwfzeqfzo  14784  supcvg  15809  zprod  15888  vdwlem6  16926  rami  16955  cshws0  17042  imasleval  17494  isssc  17774  fullestrcsetc  18110  fullsetcestrc  18125  ipodrsfi  18499  grppropd  18876  sylow1lem2  19512  sylow3lem1  19540  lsmass  19582  pj1fval  19607  efgrelexlema  19662  ablfacrplem  19980  pgpfac1lem2  19990  pgpfac1lem3  19992  pgpfac1lem4  19993  ablfac2  20004  dvdsrval  20256  dvdsrpropd  20311  znunit  21342  ellspd  21580  cnpfval  22971  cmpcov  23126  cmpsublem  23136  cmpsub  23137  tgcmp  23138  uncmp  23140  hauscmplem  23143  1stcfb  23182  2ndcctbss  23192  1stcelcls  23198  llyi  23211  nllyi  23212  cldllycmp  23232  ptrescn  23376  isufl  23650  fmid  23697  alexsublem  23781  alexsubb  23783  alexsubALTlem4  23787  alexsubALT  23788  cnextfres1  23805  tsmsf1o  23882  utopval  23970  imasf1oxms  24231  bndth  24717  ovolicc2  25284  ellimc2  25639  limcflf  25643  plyval  25956  aannenlem1  26091  aannenlem2  26092  ulm2  26147  elmade2  27615  elntg2  28525  uhgrvtxedgiedgb  28678  nb3grprlem2  28920  cplgrop  28976  cusgrexi  28982  structtocusgr  28985  1egrvtxdg0  29050  wwlksnextsurj  29436  erclwwlknsym  29605  erclwwlkntr  29606  hashecclwwlkn1  29612  umgrhashecclwwlk  29613  nfrgr2v  29807  isplig  30011  pjhth  30928  pjhfval  30931  pjhtheu2  30951  rspsnel  32773  lsmssass  32801  0ringirng  33057  iscref  33137  crefeq  33138  issros  33486  eulerpartlemgh  33690  ballotlemfc0  33804  ballotlemfcc  33805  ispconn  34527  satfv1  34667  satfvsucsuc  34669  br8  35045  br6  35046  br4  35047  wsuclem  35116  brsegle  35399  hilbert1.1  35445  limsucncmpi  35646  pibt2  36614  poimirlem24  36828  poimirlem25  36829  poimirlem27  36831  poimirlem28  36832  volsupnfl  36849  isgrpda  37139  isdrngo2  37142  lcvfbr  38206  lkrlspeqN  38357  pointsetN  38928  dia1dim2  40249  dib1dim2  40355  diclspsn  40381  dih1dimatlem  40516  lcfrvalsnN  40728  mapdpglem3  40862  mapdpglem26  40885  mapdpglem27  40886  prjspnerlem  41674  0prjspn  41685  isnacs  41757  eldioph  41811  islssfg  42127  itgoval  42218  uzubioo2  44593  limsupre3uzlem  44762  limsupre3uz  44763  limsupreuz  44764  limsupreuzmpt  44766  liminflelimsuplem  44802  liminflelimsup  44803  liminfreuz  44830  stoweidlem50  45077  stoweidlem57  45084  iccelpart  46412  fargshiftfo  46421  lco0  47208  iscnrm3r  47681