Theorem rexeqdv 3335

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-rex 3077

This theorem is referenced by:  rexeqtrdv  3337  rexeqtrrdv  3339  rexeqbidva  3341  fnunirn  7291  oarec  8618  fival  9481  marypha1lem  9502  marypha1  9503  wemapwe  9766  scshwfzeqfzo  14875  supcvg  15904  zprod  15985  vdwlem6  17033  rami  17062  cshws0  17149  imasleval  17601  isssc  17881  fullestrcsetc  18220  fullsetcestrc  18235  ipodrsfi  18609  grppropd  18991  sylow1lem2  19641  sylow3lem1  19669  lsmass  19711  pj1fval  19736  efgrelexlema  19791  pgpfac1lem2  20119  pgpfac1lem3  20121  pgpfac1lem4  20122  dvdsrval  20387  dvdsrpropd  20442  elrspsn  21273  znunit  21605  ellspd  21845  cnpfval  23263  cmpcov  23418  cmpsublem  23428  cmpsub  23429  tgcmp  23430  uncmp  23432  hauscmplem  23435  1stcfb  23474  llyi  23503  nllyi  23504  cldllycmp  23524  ptrescn  23668  isufl  23942  fmid  23989  alexsublem  24073  alexsubb  24075  alexsubALTlem4  24079  alexsubALT  24080  cnextfres1  24097  tsmsf1o  24174  utopval  24262  imasf1oxms  24523  bndth  25009  ovolicc2  25576  ellimc2  25932  limcflf  25936  plyval  26252  aannenlem1  26388  aannenlem2  26389  ulm2  26446  elmade2  27925  elntg2  29018  uhgrvtxedgiedgb  29171  nb3grprlem2  29416  cplgrop  29472  cusgrexi  29478  structtocusgr  29481  1egrvtxdg0  29547  erclwwlknsym  30102  erclwwlkntr  30103  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  nfrgr2v  30304  isplig  30508  pjhth  31425  pjhfval  31428  pjhtheu2  31448  lsmssass  33395  0ringirng  33689  iscref  33790  crefeq  33791  issros  34139  eulerpartlemgh  34343  ispconn  35191  satfv1  35331  satfvsucsuc  35333  br8  35718  br6  35719  br4  35720  wsuclem  35789  brsegle  36072  hilbert1.1  36118  limsucncmpi  36411  pibt2  37383  poimirlem24  37604  poimirlem25  37605  poimirlem27  37607  poimirlem28  37608  volsupnfl  37625  isgrpda  37915  isdrngo2  37918  lcvfbr  38976  pointsetN  39698  dia1dim2  41019  dib1dim2  41125  diclspsn  41151  dih1dimatlem  41286  lcfrvalsnN  41498  mapdpglem3  41632  mapdpglem26  41655  mapdpglem27  41656  prjspnerlem  42572  0prjspn  42583  isnacs  42660  eldioph  42714  islssfg  43027  itgoval  43118  uzubioo2  45487  limsupre3uzlem  45656  limsupre3uz  45657  limsupreuz  45658  limsupreuzmpt  45660  liminflelimsuplem  45696  liminflelimsup  45697  liminfreuz  45724  stoweidlem50  45971  stoweidlem57  45978  iccelpart  47307  fargshiftfo  47316  lco0  48156  iscnrm3r  48628