Theorem ineq1i 4170

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

Syntax hints:   = wceq 1542   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910

This theorem is referenced by:  in12  4183  inindi  4189  dfrab3  4273  dfif5  4498  disjpr2  4672  disjtpsn  4674  disjtp2  4675  resres  5959  imainrect  6147  predidm  6292  fresaun  6713  fresaunres2  6714  ssenen  9091  hartogslem1  9459  prinfzo0  13626  leiso  14394  f1oun2prg  14852  smumul  16432  setsfun  17110  setsfun0  17111  firest  17364  lsmdisj2r  19626  frgpuplem  19713  ltbwe  22011  tgrest  23115  fiuncmp  23360  ptclsg  23571  metnrmlem3  24818  mbfid  25604  ppi1  27142  cht1  27143  ppiub  27183  lrrecse  27950  lrrecpred  27952  chdmj2i  31570  chjassi  31574  pjoml2i  31673  pjoml4i  31675  cmcmlem  31679  mayetes3i  31817  cvmdi  32412  atomli  32470  atabsi  32489  uniin1  32638  disjuniel  32684  imadifxp  32688  gtiso  32791  preiman0  32800  nn0disj01  32910  evlextv  33719  esplyind  33752  prsss  34094  ordtrest2NEW  34101  esumnul  34226  measinblem  34398  eulerpartlemt  34549  ballotlem2  34667  ballotlemfp1  34670  ballotlemfval0  34674  chtvalz  34807  fmla0disjsuc  35614  mthmpps  35798  dffv5  36138  bj-sscon  37277  bj-discrmoore  37364  mblfinlem2  37909  ismblfin  37912  mbfposadd  37918  itg2addnclem2  37923  asindmre  37954  abeqin  38505  xrnres  38676  redundeq1  38964  refrelsredund4  38967  dfpetparts2  39223  dfpeters2  39225  diophrw  43116  dnwech  43405  lmhmlnmsplit  43444  rp-fakeuninass  43872  iunrelexp0  44058  nznngen  44672  uzinico2  45921  limsup0  46052  limsupvaluz  46066  sge0sn  46737  31prm  47957