Theorem rexeqdv 3365

Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)

Hypothesis

Ref	Expression
raleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rexeqdv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rexeqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rexeq 3359	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∃wrex 3107

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-rex 3112

This theorem is referenced by:  rexeqbidva  3371  fnunirn  6990  oarec  8171  fival  8860  marypha1lem  8881  marypha1  8882  wemapwe  9144  zornn0g  9916  scshwfzeqfzo  14179  supcvg  15203  zprod  15283  vdwlem6  16312  rami  16341  cshws0  16427  imasleval  16806  isssc  17082  fullestrcsetc  17393  fullsetcestrc  17408  ipodrsfi  17765  grppropd  18110  sylow1lem2  18716  sylow3lem1  18744  lsmass  18787  pj1fval  18812  efgrelexlema  18867  ablfacrplem  19180  pgpfac1lem2  19190  pgpfac1lem3  19192  pgpfac1lem4  19193  ablfac2  19204  dvdsrval  19391  dvdsrpropd  19442  znunit  20255  ellspd  20491  cnpfval  21839  cmpcov  21994  cmpsublem  22004  cmpsub  22005  tgcmp  22006  uncmp  22008  hauscmplem  22011  1stcfb  22050  2ndcctbss  22060  1stcelcls  22066  llyi  22079  nllyi  22080  cldllycmp  22100  ptrescn  22244  isufl  22518  fmid  22565  alexsublem  22649  alexsubb  22651  alexsubALTlem4  22655  alexsubALT  22656  cnextfres1  22673  tsmsf1o  22750  utopval  22838  imasf1oxms  23096  bndth  23563  ovolicc2  24126  ellimc2  24480  limcflf  24484  plyval  24790  aannenlem1  24924  aannenlem2  24925  ulm2  24980  elntg2  26779  uhgrvtxedgiedgb  26929  nb3grprlem2  27171  cplgrop  27227  cusgrexi  27233  structtocusgr  27236  1egrvtxdg0  27301  wwlksnextsurj  27686  erclwwlknsym  27855  erclwwlkntr  27856  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  nfrgr2v  28057  isplig  28259  pjhth  29176  pjhfval  29179  pjhtheu2  29199  rspsnel  30987  lsmssass  31009  iscref  31197  crefeq  31198  issros  31544  eulerpartlemgh  31746  ballotlemfc0  31860  ballotlemfcc  31861  ispconn  32583  satfv1  32723  satfvsucsuc  32725  br8  33105  br6  33106  br4  33107  wsuclem  33225  brsegle  33682  hilbert1.1  33728  limsucncmpi  33906  pibt2  34834  poimirlem24  35081  poimirlem25  35082  poimirlem27  35084  poimirlem28  35085  volsupnfl  35102  isgrpda  35393  isdrngo2  35396  lcvfbr  36316  lkrlspeqN  36467  pointsetN  37037  dia1dim2  38358  dib1dim2  38464  diclspsn  38490  dih1dimatlem  38625  lcfrvalsnN  38837  mapdpglem3  38971  mapdpglem26  38994  mapdpglem27  38995  prjspnval2  39611  0prjspn  39614  isnacs  39645  eldioph  39699  islssfg  40014  itgoval  40105  uzubioo2  42206  limsupre3uzlem  42377  limsupre3uz  42378  limsupreuz  42379  limsupreuzmpt  42381  liminflelimsuplem  42417  liminflelimsup  42418  liminfreuz  42445  stoweidlem50  42692  stoweidlem57  42699  iccelpart  43950  fargshiftfo  43959  lco0  44836