Theorem ineq1i 4115

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

Hypothesis

Ref	Expression
ineq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
ineq1i	⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)

Proof of Theorem ineq1i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		ineq1 4111	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)

Syntax hints:   = wceq 1538   ∩ cin 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-in 3867

This theorem is referenced by:  in12  4127  inindi  4133  dfrab3  4214  dfif5  4439  disjpr2  4609  disjtpsn  4611  disjtp2  4612  resres  5840  imainrect  6014  predidm  6152  fresaun  6538  fresaunres2  6539  ssenen  8718  hartogslem1  9044  prinfzo0  13130  leiso  13874  f1oun2prg  14331  smumul  15897  setsfun  16581  setsfun0  16582  firest  16769  lsmdisj2r  18883  frgpuplem  18970  ltbwe  20809  tgrest  21864  fiuncmp  22109  ptclsg  22320  metnrmlem3  23567  mbfid  24340  ppi1  25853  cht1  25854  ppiub  25892  chdmj2i  29369  chjassi  29373  pjoml2i  29472  pjoml4i  29474  cmcmlem  29478  mayetes3i  29616  cvmdi  30211  atomli  30269  atabsi  30288  uniin1  30418  disjuniel  30463  imadifxp  30467  gtiso  30561  preiman0  30570  prsss  31391  ordtrest2NEW  31398  esumnul  31539  measinblem  31711  eulerpartlemt  31861  ballotlem2  31978  ballotlemfp1  31981  ballotlemfval0  31985  chtvalz  32132  fmla0disjsuc  32880  mthmpps  33064  lrrecse  33673  lrrecpred  33675  dffv5  33801  bj-sscon  34772  bj-discrmoore  34832  mblfinlem2  35401  ismblfin  35404  mbfposadd  35410  itg2addnclem2  35415  asindmre  35446  abeqin  35980  xrnres  36116  redundeq1  36330  refrelsredund4  36333  diophrw  40101  dnwech  40393  lmhmlnmsplit  40432  rp-fakeuninass  40625  iunrelexp0  40804  nznngen  41421  uzinico2  42593  limsup0  42730  limsupvaluz  42744  sge0sn  43412  31prm  44510