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  4446  inex1g  4729  reseq1  5311  sspred  5605  isofrlem  6490  qsdisj  7711  fiint  8122  elfiun  8219  dffi3  8220  inf3lema  8404  dfac5lem5  8833  kmlem12  8866  kmlem14  8868  fin23lem24  9027  fin23lem26  9030  fin23lem23  9031  fin23lem22  9032  fin23lem27  9033  ingru  9516  uzin2  13932  incexclem  14407  elrestr  15912  firest  15916  inopn  20529  isbasisg  20562  basis1  20565  basis2  20566  tgval  20570  fctop  20618  cctop  20620  ntrfval  20638  elcls  20687  clsndisj  20689  elcls3  20697  neindisj2  20737  tgrest  20773  restco  20778  restsn  20784  restcld  20786  restcldi  20787  restopnb  20789  neitr  20794  restcls  20795  ordtbaslem  20802  ordtrest2lem  20817  hausnei2  20967  cnhaus  20968  regsep2  20990  dishaus  20996  ordthauslem  20997  cmpsublem  21012  cmpsub  21013  nconsubb  21036  consubclo  21037  1stcelcls  21074  islly  21081  cldllycmp  21108  lly1stc  21109  locfincmp  21139  elkgen  21149  ptclsg  21228  dfac14lem  21230  txrest  21244  pthaus  21251  txhaus  21260  xkohaus  21266  xkoptsub  21267  regr1lem  21352  isfbas  21443  fbasssin  21450  fbun  21454  isfil  21461  fbunfip  21483  fgval  21484  filcon  21497  uzrest  21511  isufil2  21522  hauspwpwf1  21601  fclsopni  21629  fclsnei  21633  fclsrest  21638  fcfnei  21649  fcfneii  21651  tsmsfbas  21741  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ust0  21833  trust  21843  restutopopn  21852  lpbl  22118  methaus  22135  metrest  22139  restmetu  22185  qtopbaslem  22372  qdensere  22383  xrtgioo  22417  metnrmlem3  22472  icoopnst  22546  iocopnst  22547  ovolicc2lem2  23093  ovolicc2lem5  23096  mblsplit  23107  limcnlp  23448  ellimc3  23449  limcflf  23451  limciun  23464  ig1pval  23736  shincl  27624  shmodi  27633  omlsi  27647  pjoml  27679  chm0  27734  chincl  27742  chdmm1  27768  ledi  27783  cmbr  27827  cmbr3  27851  mdbr  28537  dmdmd  28543  dmdi  28545  dmdbr3  28548  dmdbr4  28549  mdslmd1lem4  28571  cvmd  28579  cvexch  28617  dmdbr6ati  28666  mddmdin0i  28674  difeq  28739  ofpreima2  28849  ordtrest2NEWlem  29296  inelsros  29568  diffiunisros  29569  measvuni  29604  measinb  29611  inelcarsg  29700  carsgclctunlem2  29708  totprob  29816  ballotlemgval  29912  cvmscbv  30494  cvmsdisj  30506  cvmsss2  30510  nepss  30854  brapply  31215  opnbnd  31490  isfne  31504  tailfb  31542  bj-restsn  32216  bj-restpw  32226  bj-rest0  32227  bj-restb  32228  ptrest  32578  poimirlem30  32609  mblfinlem2  32617  bndss  32755  lcvexchlem4  33342  fipjust  36889  ntrkbimka  37356  ntrk0kbimka  37357  clsk3nimkb  37358  isotone2  37367  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  elrestd  38322  islptre  38686  islpcn  38706  subsaliuncllem  39251  subsaliuncl  39252  nnfoctbdjlem  39348  caragensplit  39390  vonvolmbllem  39550  vonvolmbl  39551  incsmflem  39628  decsmflem  39652  smflimlem2  39658  smflimlem3  39659  smflim  39663  uzlidlring  41719  rngcvalALTV  41753  rngcval  41754  ringcvalALTV  41799  ringcval  41800