Theorem ineq1i 4168

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

Syntax hints:   = wceq 1541   ∩ cin 3900

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908

This theorem is referenced by:  in12  4181  inindi  4187  dfrab3  4271  dfif5  4496  disjpr2  4670  disjtpsn  4672  disjtp2  4673  resres  5951  imainrect  6139  predidm  6284  fresaun  6705  fresaunres2  6706  ssenen  9079  hartogslem1  9447  prinfzo0  13614  leiso  14382  f1oun2prg  14840  smumul  16420  setsfun  17098  setsfun0  17099  firest  17352  lsmdisj2r  19614  frgpuplem  19701  ltbwe  21999  tgrest  23103  fiuncmp  23348  ptclsg  23559  metnrmlem3  24806  mbfid  25592  ppi1  27130  cht1  27131  ppiub  27171  lrrecse  27938  lrrecpred  27940  chdmj2i  31557  chjassi  31561  pjoml2i  31660  pjoml4i  31662  cmcmlem  31666  mayetes3i  31804  cvmdi  32399  atomli  32457  atabsi  32476  uniin1  32626  disjuniel  32672  imadifxp  32676  gtiso  32780  preiman0  32789  nn0disj01  32899  evlextv  33707  esplyind  33731  prsss  34073  ordtrest2NEW  34080  esumnul  34205  measinblem  34377  eulerpartlemt  34528  ballotlem2  34646  ballotlemfp1  34649  ballotlemfval0  34653  chtvalz  34786  fmla0disjsuc  35592  mthmpps  35776  dffv5  36116  bj-sscon  37230  bj-discrmoore  37316  mblfinlem2  37859  ismblfin  37862  mbfposadd  37868  itg2addnclem2  37873  asindmre  37904  abeqin  38450  xrnres  38610  redundeq1  38886  refrelsredund4  38889  diophrw  43001  dnwech  43290  lmhmlnmsplit  43329  rp-fakeuninass  43757  iunrelexp0  43943  nznngen  44557  uzinico2  45807  limsup0  45938  limsupvaluz  45952  sge0sn  46623  31prm  47843