Theorem ineq1i 4166

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

Syntax hints:   = wceq 1541   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-in 3906

This theorem is referenced by:  in12  4179  inindi  4185  dfrab3  4269  dfif5  4494  disjpr2  4668  disjtpsn  4670  disjtp2  4671  resres  5949  imainrect  6137  predidm  6282  fresaun  6703  fresaunres2  6704  ssenen  9077  hartogslem1  9445  prinfzo0  13612  leiso  14380  f1oun2prg  14838  smumul  16418  setsfun  17096  setsfun0  17097  firest  17350  lsmdisj2r  19612  frgpuplem  19699  ltbwe  21997  tgrest  23101  fiuncmp  23346  ptclsg  23557  metnrmlem3  24804  mbfid  25590  ppi1  27128  cht1  27129  ppiub  27169  lrrecse  27912  lrrecpred  27914  chdmj2i  31506  chjassi  31510  pjoml2i  31609  pjoml4i  31611  cmcmlem  31615  mayetes3i  31753  cvmdi  32348  atomli  32406  atabsi  32425  uniin1  32575  disjuniel  32621  imadifxp  32625  gtiso  32729  preiman0  32738  nn0disj01  32848  evlextv  33656  esplyind  33680  prsss  34022  ordtrest2NEW  34029  esumnul  34154  measinblem  34326  eulerpartlemt  34477  ballotlem2  34595  ballotlemfp1  34598  ballotlemfval0  34602  chtvalz  34735  fmla0disjsuc  35541  mthmpps  35725  dffv5  36065  bj-sscon  37173  bj-discrmoore  37255  mblfinlem2  37798  ismblfin  37801  mbfposadd  37807  itg2addnclem2  37812  asindmre  37843  abeqin  38389  xrnres  38549  redundeq1  38825  refrelsredund4  38828  diophrw  42943  dnwech  43232  lmhmlnmsplit  43271  rp-fakeuninass  43699  iunrelexp0  43885  nznngen  44499  uzinico2  45749  limsup0  45880  limsupvaluz  45894  sge0sn  46565  31prm  47785