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 1559   ∩ cin 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3909

This theorem is referenced by:  in12  4178  inindi  4184  dfrab3  4269  dfif5  4494  disjpr2  4669  disjtpsn  4671  disjtp2  4672  resres  5974  imainrect  6162  predidm  6308  fresaun  6730  fresaunres2  6731  ssenen  9117  hartogslem1  9484  prinfzo0  13698  leiso  14466  f1oun2prg  14924  smumul  16518  setsfun  17198  setsfun0  17199  firest  17452  lsmdisj2r  19716  frgpuplem  19803  ltbwe  22085  tgrest  23207  fiuncmp  23452  ptclsg  23663  metnrmlem3  24910  mbfid  25685  ppi1  27216  cht1  27217  ppiub  27256  lrrecse  28023  lrrecpred  28025  chdmj2i  31642  chjassi  31646  pjoml2i  31745  pjoml4i  31747  cmcmlem  31751  mayetes3i  31889  cvmdi  32484  atomli  32542  atabsi  32561  uniin1  32711  disjuniel  32757  imadifxp  32761  gtiso  32864  preiman0  32873  nn0disj01  32982  evlextv  33800  prsss  34174  ordtrest2NEW  34181  esumnul  34306  measinblem  34478  eulerpartlemt  34629  ballotlem2  34747  ballotlemfp1  34750  ballotlemfval0  34754  chtvalz  34884  fmla0disjsuc  35709  mthmpps  35893  dffv5  36233  bj-sscon  37475  bj-discrmoore  37562  mblfinlem2  38118  ismblfin  38121  mbfposadd  38127  itg2addnclem2  38132  asindmre  38163  abeqin  38714  xrnres  38885  redundeq1  39173  refrelsredund4  39176  dfpetparts2  39432  dfpeters2  39434  diophrw  43301  dnwech  43586  lmhmlnmsplit  43625  rp-fakeuninass  44053  iunrelexp0  44239  nznngen  44853  uzinico2  46098  limsup0  46229  limsupvaluz  46243  sge0sn  46914  31prm  48167