Theorem ineq1i 4112

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

This proof depends on syntax axioms:   = wceq 1569   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4090

This theorem is used by:  in12  4124  inindi  4130  dfrab3  4263  dfif5  4498  disjpr2  4670  disjtpsn  4672  disjtp2  4673  uniin1  5032  resres  5983  imainrect  6174  predidm  6331  fresaun  6756  fresaunres2  6757  ssenen  9175  hartogslem1  9541  prinfzo0  13838  leiso  14609  f1oun2prg  15075  smumul  16670  setsfun  17356  setsfun0  17357  firest  17610  lsmdisj2r  19906  frgpuplem  19993  ltbwe  22360  tgrest  23484  fiuncmp  23729  ptclsg  23941  metnrmlem3  25188  mbfid  25963  ppi1  27498  cht1  27499  ppiub  27538  lrrecse  28335  lrrecpred  28337  chdmj2i  32091  chjassi  32095  pjoml2i  32194  pjoml4i  32196  cmcmlem  32200  mayetes3i  32338  cvmdi  32933  atomli  32991  atabsi  33010  disjuniel  33240  imadifxp  33244  gtiso  33343  preiman0  33352  nn0disj01  33458  evlextv  34222  prsss  34596  ordtrest2NEW  34603  esumnul  34728  measinblem  34901  eulerpartlemt  35051  ballotlem2  35169  ballotlemfp1  35172  ballotlemfval0  35176  chtvalz  35306  dfscott3  35799  fmla0disjsuc  36251  mthmpps  36435  dffv5  36780  bj-sscon  38036  bj-discrmoore  38138  mblfinlem2  38683  ismblfin  38686  mbfposadd  38692  itg2addnclem2  38697  asindmre  38728  abeqin  39293  xrnres  39464  redundeq1  39752  refrelsredund4  39755  dfpetparts2  40011  dfpeters2  40013  diophrw  43877  dnwech  44162  lmhmlnmsplit  44196  rp-fakeuninass  44624  iunrelexp0  44809  nznngen  45407  uzinico2  46680  limsup0  46811  limsupvaluz  46825  sge0sn  47496  31prm  48789