Theorem ineq1i 3772

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

Syntax hints:   = wceq 1475   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  in12  3786  inindi  3792  dfrab3  3861  dfif5  4052  disjpr2  4194  disjpr2OLD  4195  resres  5329  imainrect  5494  predidm  5619  fresaun  5988  fresaunres2  5989  ssenen  8019  hartogslem1  8330  leiso  13100  f1oun2prg  13512  smumul  15053  setsfun  15725  setsfun0  15726  firest  15916  lsmdisj2r  17921  frgpuplem  18008  ltbwe  19293  tgrest  20773  fiuncmp  21017  ptclsg  21228  metnrmlem3  22472  mbfid  23209  ppi1  24690  cht1  24691  ppiub  24729  cusgrasizeindslem1  26002  chdmj2i  27725  chjassi  27729  pjoml2i  27828  pjoml4i  27830  cmcmlem  27834  mayetes3i  27972  cvmdi  28567  atomli  28625  atabsi  28644  uniin1  28750  disjuniel  28792  imadifxp  28796  gtiso  28861  prsss  29290  ordtrest2NEW  29297  esumnul  29437  measinblem  29610  eulerpartlemt  29760  ballotlem2  29877  ballotlemfp1  29880  ballotlemfval0  29884  mthmpps  30733  dffv5  31201  mblfinlem2  32617  ismblfin  32620  mbfposadd  32627  itg2addnclem2  32632  asindmre  32665  diophrw  36340  dnwech  36636  lmhmlnmsplit  36675  rp-fakeuninass  36881  iunrelexp0  37013  nznngen  37537  sge0sn  39272  31prm  40050  prinfzo0  40363