Theorem ineq1i 4161

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

Syntax hints:   = wceq 1541   ∩ cin 3896

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3904

This theorem is referenced by:  in12  4174  inindi  4180  dfrab3  4264  dfif5  4487  disjpr2  4661  disjtpsn  4663  disjtp2  4664  resres  5936  imainrect  6123  predidm  6268  fresaun  6689  fresaunres2  6690  ssenen  9059  hartogslem1  9423  prinfzo0  13593  leiso  14361  f1oun2prg  14819  smumul  16399  setsfun  17077  setsfun0  17078  firest  17331  lsmdisj2r  19592  frgpuplem  19679  ltbwe  21974  tgrest  23069  fiuncmp  23314  ptclsg  23525  metnrmlem3  24772  mbfid  25558  ppi1  27096  cht1  27097  ppiub  27137  lrrecse  27880  lrrecpred  27882  chdmj2i  31454  chjassi  31458  pjoml2i  31557  pjoml4i  31559  cmcmlem  31563  mayetes3i  31701  cvmdi  32296  atomli  32354  atabsi  32373  uniin1  32523  disjuniel  32569  imadifxp  32573  gtiso  32674  preiman0  32683  nn0disj01  32793  prsss  33921  ordtrest2NEW  33928  esumnul  34053  measinblem  34225  eulerpartlemt  34376  ballotlem2  34494  ballotlemfp1  34497  ballotlemfval0  34501  chtvalz  34634  fmla0disjsuc  35434  mthmpps  35618  dffv5  35958  bj-sscon  37063  bj-discrmoore  37145  mblfinlem2  37698  ismblfin  37701  mbfposadd  37707  itg2addnclem2  37712  asindmre  37743  abeqin  38287  xrnres  38434  redundeq1  38666  refrelsredund4  38669  diophrw  42792  dnwech  43081  lmhmlnmsplit  43120  rp-fakeuninass  43549  iunrelexp0  43735  nznngen  44349  uzinico2  45601  limsup0  45732  limsupvaluz  45746  sge0sn  46417  31prm  47628