Theorem rexeqdv 3340

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexeqbidva  3346  fnunirn  7108  oarec  8355  fival  9101  marypha1lem  9122  marypha1  9123  wemapwe  9385  zornn0g  10192  scshwfzeqfzo  14467  supcvg  15496  zprod  15575  vdwlem6  16615  rami  16644  cshws0  16731  imasleval  17169  isssc  17449  fullestrcsetc  17784  fullsetcestrc  17799  ipodrsfi  18172  grppropd  18509  sylow1lem2  19119  sylow3lem1  19147  lsmass  19190  pj1fval  19215  efgrelexlema  19270  ablfacrplem  19583  pgpfac1lem2  19593  pgpfac1lem3  19595  pgpfac1lem4  19596  ablfac2  19607  dvdsrval  19802  dvdsrpropd  19853  znunit  20683  ellspd  20919  cnpfval  22293  cmpcov  22448  cmpsublem  22458  cmpsub  22459  tgcmp  22460  uncmp  22462  hauscmplem  22465  1stcfb  22504  2ndcctbss  22514  1stcelcls  22520  llyi  22533  nllyi  22534  cldllycmp  22554  ptrescn  22698  isufl  22972  fmid  23019  alexsublem  23103  alexsubb  23105  alexsubALTlem4  23109  alexsubALT  23110  cnextfres1  23127  tsmsf1o  23204  utopval  23292  imasf1oxms  23551  bndth  24027  ovolicc2  24591  ellimc2  24946  limcflf  24950  plyval  25259  aannenlem1  25393  aannenlem2  25394  ulm2  25449  elntg2  27256  uhgrvtxedgiedgb  27409  nb3grprlem2  27651  cplgrop  27707  cusgrexi  27713  structtocusgr  27716  1egrvtxdg0  27781  wwlksnextsurj  28166  erclwwlknsym  28335  erclwwlkntr  28336  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  nfrgr2v  28537  isplig  28739  pjhth  29656  pjhfval  29659  pjhtheu2  29679  rspsnel  31469  lsmssass  31492  iscref  31696  crefeq  31697  issros  32043  eulerpartlemgh  32245  ballotlemfc0  32359  ballotlemfcc  32360  ispconn  33085  satfv1  33225  satfvsucsuc  33227  br8  33629  br6  33630  br4  33631  wsuclem  33746  elmade2  33979  brsegle  34337  hilbert1.1  34383  limsucncmpi  34561  pibt2  35515  poimirlem24  35728  poimirlem25  35729  poimirlem27  35731  poimirlem28  35732  volsupnfl  35749  isgrpda  36040  isdrngo2  36043  lcvfbr  36961  lkrlspeqN  37112  pointsetN  37682  dia1dim2  39003  dib1dim2  39109  diclspsn  39135  dih1dimatlem  39270  lcfrvalsnN  39482  mapdpglem3  39616  mapdpglem26  39639  mapdpglem27  39640  prjspnerlem  40377  0prjspn  40386  isnacs  40442  eldioph  40496  islssfg  40811  itgoval  40902  uzubioo2  42997  limsupre3uzlem  43166  limsupre3uz  43167  limsupreuz  43168  limsupreuzmpt  43170  liminflelimsuplem  43206  liminflelimsup  43207  liminfreuz  43234  stoweidlem50  43481  stoweidlem57  43488  iccelpart  44773  fargshiftfo  44782  lco0  45656  iscnrm3r  46130