Theorem ineq1i 4116

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

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094

This theorem is used by:  in12  4128  inindi  4134  dfrab3  4267  dfif5  4502  disjpr2  4675  disjtpsn  4677  disjtp2  4679  uniin1  5038  resres  5999  imainrect  6191  predidm  6355  fresaun  6783  fresaunres2  6784  ssenen  9208  hartogslem1  9573  prinfzo0  13873  leiso  14645  f1oun2prg  15111  smumul  16707  setsfun  17393  setsfun0  17394  firest  17653  lsmdisj2r  19950  frgpuplem  20037  ltbwe  22408  tgrest  23532  fiuncmp  23777  ptclsg  23989  metnrmlem3  25236  mbfid  26011  ppi1  27548  cht1  27549  ppiub  27588  lrrecse  28385  lrrecpred  28387  chdmj2i  32141  chjassi  32145  pjoml2i  32244  pjoml4i  32246  cmcmlem  32250  mayetes3i  32388  cvmdi  32983  atomli  33041  atabsi  33060  disjuniel  33289  imadifxp  33293  gtiso  33391  preiman0  33400  nn0disj01  33506  evlextv  34285  prsss  34659  ordtrest2NEW  34666  esumnul  34791  measinblem  34964  eulerpartlemt  35114  ballotlem2  35232  ballotlemfp1  35235  ballotlemfval0  35239  chtvalz  35369  dfscott3  35868  fmla0disjsuc  36371  mthmpps  36555  dffv5  36901  bj-sscon  38157  bj-discrmoore  38302  mblfinlem2  38844  ismblfin  38847  mbfposadd  38853  itg2addnclem2  38858  asindmre  38889  abeqin  39452  xrnres  39623  redundeq1  39911  refrelsredund4  39914  dfpetparts2  40170  dfpeters2  40172  diophrw  44036  dnwech  44321  lmhmlnmsplit  44355  rp-fakeuninass  44778  iunrelexp0  44963  nznngen  45561  uzinico2  46846  limsup0  46977  limsupvaluz  46991  sge0sn  47662  31prm  48955