Theorem ineq1 3769

Description: Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)

Assertion

Ref	Expression
ineq1	⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Proof of Theorem ineq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2677	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 737	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3758	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3758	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 302	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	eqrdv 2608	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  ineq2  3770  ineq12  3771  ineq1i  3772  ineq1d  3775  unineq  3836  dfrab3ss  3864  intprg  4441  inex1g  4724  reseq1  5298  sspred  5591  isofrlem  6468  qsdisj  7689  fiint  8100  elfiun  8197  dffi3  8198  inf3lema  8382  dfac5lem5  8811  kmlem12  8844  kmlem14  8846  fin23lem24  9005  fin23lem26  9008  fin23lem23  9009  fin23lem22  9010  fin23lem27  9011  ingru  9494  uzin2  13881  incexclem  14356  elrestr  15861  firest  15865  inopn  20477  isbasisg  20510  basis1  20513  basis2  20514  tgval  20518  fctop  20566  cctop  20568  ntrfval  20586  elcls  20635  clsndisj  20637  elcls3  20645  neindisj2  20685  tgrest  20721  restco  20726  restsn  20732  restcld  20734  restcldi  20735  restopnb  20737  neitr  20742  restcls  20743  ordtbaslem  20750  ordtrest2lem  20765  hausnei2  20915  cnhaus  20916  regsep2  20938  dishaus  20944  ordthauslem  20945  cmpsublem  20960  cmpsub  20961  nconsubb  20984  consubclo  20985  1stcelcls  21022  islly  21029  cldllycmp  21056  lly1stc  21057  locfincmp  21087  elkgen  21097  ptclsg  21176  dfac14lem  21178  txrest  21192  pthaus  21199  txhaus  21208  xkohaus  21214  xkoptsub  21215  regr1lem  21300  isfbas  21391  fbasssin  21398  fbun  21402  isfil  21409  fbunfip  21431  fgval  21432  filcon  21445  uzrest  21459  isufil2  21470  hauspwpwf1  21549  fclsopni  21577  fclsnei  21581  fclsrest  21586  fcfnei  21597  fcfneii  21599  tsmsfbas  21689  ustincl  21769  ustdiag  21770  ustinvel  21771  ustexhalf  21772  ust0  21781  trust  21791  restutopopn  21800  lpbl  22066  methaus  22083  metrest  22087  restmetu  22133  qtopbaslem  22320  qdensere  22331  xrtgioo  22365  metnrmlem3  22420  icoopnst  22494  iocopnst  22495  ovolicc2lem2  23038  ovolicc2lem5  23041  mblsplit  23052  limcnlp  23393  ellimc3  23394  limcflf  23396  limciun  23409  ig1pval  23681  shincl  27418  shmodi  27427  omlsi  27441  pjoml  27473  chm0  27528  chincl  27536  chdmm1  27562  ledi  27577  cmbr  27621  cmbr3  27645  mdbr  28331  dmdmd  28337  dmdi  28339  dmdbr3  28342  dmdbr4  28343  mdslmd1lem4  28365  cvmd  28373  cvexch  28411  dmdbr6ati  28460  mddmdin0i  28468  difeq  28533  ofpreima2  28643  ordtrest2NEWlem  29090  inelsros  29362  diffiunisros  29363  measvuni  29398  measinb  29405  inelcarsg  29494  carsgclctunlem2  29502  totprob  29610  ballotlemgval  29706  cvmscbv  30288  cvmsdisj  30300  cvmsss2  30304  nepss  30648  brapply  31009  opnbnd  31284  isfne  31298  tailfb  31336  bj-restsn  32010  bj-restpw  32020  bj-rest0  32021  bj-restb  32022  ptrest  32372  poimirlem30  32403  mblfinlem2  32411  bndss  32549  lcvexchlem4  33136  fipjust  36683  ntrkbimka  37150  ntrk0kbimka  37151  clsk3nimkb  37152  isotone2  37161  ntrclskb  37181  ntrclsk3  37182  ntrclsk13  37183  elrestd  38116  islptre  38480  islpcn  38500  subsaliuncllem  39045  subsaliuncl  39046  nnfoctbdjlem  39142  caragensplit  39184  vonvolmbllem  39344  vonvolmbl  39345  incsmflem  39422  decsmflem  39446  smflimlem2  39452  smflimlem3  39453  smflim  39457  uzlidlring  41711  rngcvalALTV  41745  rngcval  41746  ringcvalALTV  41791  ringcval  41792