Theorem rexeqdv 3341

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601  ∃wrex 3091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-clel 2774  df-rex 3096

This theorem is referenced by:  rexeqbidvOLD  3349  rexeqbidva  3351  fnunirn  6783  oarec  7926  fival  8606  marypha1lem  8627  marypha1  8628  wemapwe  8891  zornn0g  9662  scshwfzeqfzo  13977  supcvg  14992  zprod  15070  vdwlem6  16094  rami  16123  cshws0  16207  imasleval  16587  isssc  16865  fullestrcsetc  17177  fullsetcestrc  17192  ipodrsfi  17549  grppropd  17824  sylow1lem2  18398  sylow3lem1  18426  lsmass  18467  pj1fval  18491  efgrelexlema  18548  ablfacrplem  18851  pgpfac1lem2  18861  pgpfac1lem3  18863  pgpfac1lem4  18864  ablfac2  18875  dvdsrval  19032  dvdsrpropd  19083  znunit  20307  ellspd  20545  cnpfval  21446  cmpcov  21601  cmpsublem  21611  cmpsub  21612  tgcmp  21613  uncmp  21615  hauscmplem  21618  1stcfb  21657  2ndcctbss  21667  1stcelcls  21673  llyi  21686  nllyi  21687  cldllycmp  21707  ptrescn  21851  isufl  22125  fmid  22172  alexsublem  22256  alexsubb  22258  alexsubALTlem4  22262  alexsubALT  22263  cnextfres1  22280  tsmsf1o  22356  utopval  22444  imasf1oxms  22702  bndth  23165  ovolicc2  23726  ellimc2  24078  limcflf  24082  plyval  24386  aannenlem1  24520  aannenlem2  24521  ulm2  24576  ishpg  26107  elntg2  26334  uhgrvtxedgiedgb  26484  uhgrvtxedgiedgbOLD  26485  nb3grprlem2  26729  cplgrop  26785  cusgrexi  26791  structtocusgr  26794  1egrvtxdg0  26859  wwlksnextsurj  27264  wwlksnextsurOLD  27269  erclwwlknsym  27468  erclwwlkntr  27469  hashecclwwlkn1  27475  umgrhashecclwwlk  27476  nfrgr2v  27680  isplig  27903  pjhth  28824  pjhfval  28827  pjhtheu2  28847  iscref  30509  crefeq  30510  issros  30836  eulerpartlemgh  31038  ballotlemfc0  31153  ballotlemfcc  31154  ispconn  31804  br8  32240  br6  32241  br4  32242  wsuclem  32359  brsegle  32804  hilbert1.1  32850  limsucncmpi  33027  poimirlem24  34059  poimirlem25  34060  poimirlem27  34062  poimirlem28  34063  volsupnfl  34080  isgrpda  34378  isdrngo2  34381  lcvfbr  35174  lkrlspeqN  35325  pointsetN  35895  dia1dim2  37216  dib1dim2  37322  diclspsn  37348  dih1dimatlem  37483  lcfrvalsnN  37695  mapdpglem3  37829  mapdpglem26  37852  mapdpglem27  37853  isnacs  38227  eldioph  38281  islssfg  38599  itgoval  38690  uzubioo2  40704  limsupre3uzlem  40875  limsupre3uz  40876  limsupreuz  40877  limsupreuzmpt  40879  liminflelimsuplem  40915  liminflelimsup  40916  liminfreuz  40943  stoweidlem50  41194  stoweidlem57  41201  iccelpart  42401  fargshiftfo  42410  lco0  43231