Theorem ineq1i 4142

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 4139	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)

Syntax hints:   = wceq 1539   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-in 3894

This theorem is referenced by:  in12  4154  inindi  4160  dfrab3  4243  dfif5  4475  disjpr2  4649  disjtpsn  4651  disjtp2  4652  resres  5904  imainrect  6084  predidm  6229  fresaun  6645  fresaunres2  6646  ssenen  8938  hartogslem1  9301  prinfzo0  13426  leiso  14173  f1oun2prg  14630  smumul  16200  setsfun  16872  setsfun0  16873  firest  17143  lsmdisj2r  19291  frgpuplem  19378  ltbwe  21245  tgrest  22310  fiuncmp  22555  ptclsg  22766  metnrmlem3  24024  mbfid  24799  ppi1  26313  cht1  26314  ppiub  26352  chdmj2i  29844  chjassi  29848  pjoml2i  29947  pjoml4i  29949  cmcmlem  29953  mayetes3i  30091  cvmdi  30686  atomli  30744  atabsi  30763  uniin1  30891  disjuniel  30936  imadifxp  30940  gtiso  31033  preiman0  31042  prsss  31866  ordtrest2NEW  31873  esumnul  32016  measinblem  32188  eulerpartlemt  32338  ballotlem2  32455  ballotlemfp1  32458  ballotlemfval0  32462  chtvalz  32609  fmla0disjsuc  33360  mthmpps  33544  lrrecse  34099  lrrecpred  34101  dffv5  34226  bj-sscon  35219  bj-discrmoore  35282  mblfinlem2  35815  ismblfin  35818  mbfposadd  35824  itg2addnclem2  35829  asindmre  35860  abeqin  36392  xrnres  36528  redundeq1  36742  refrelsredund4  36745  diophrw  40581  dnwech  40873  lmhmlnmsplit  40912  rp-fakeuninass  41123  iunrelexp0  41310  nznngen  41934  uzinico2  43100  limsup0  43235  limsupvaluz  43249  sge0sn  43917  31prm  45049