Theorem ineq1i 4169

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913

This theorem is used by:  in12  4181  inindi  4187  dfrab3  4272  dfif5  4506  disjpr2  4681  disjtpsn  4683  disjtp2  4684  uniin1  5041  resres  5993  imainrect  6181  predidm  6331  fresaun  6753  fresaunres2  6754  ssenen  9146  hartogslem1  9511  prinfzo0  13744  leiso  14514  f1oun2prg  14978  smumul  16573  setsfun  17253  setsfun0  17254  firest  17507  lsmdisj2r  19799  frgpuplem  19886  ltbwe  22245  tgrest  23366  fiuncmp  23611  ptclsg  23823  metnrmlem3  25070  mbfid  25845  ppi1  27379  cht1  27380  ppiub  27419  lrrecse  28186  lrrecpred  28188  chdmj2i  31905  chjassi  31909  pjoml2i  32008  pjoml4i  32010  cmcmlem  32014  mayetes3i  32152  cvmdi  32747  atomli  32805  atabsi  32824  disjuniel  33013  imadifxp  33017  gtiso  33117  preiman0  33126  nn0disj01  33233  evlextv  33996  prsss  34370  ordtrest2NEW  34377  esumnul  34502  measinblem  34675  eulerpartlemt  34826  ballotlem2  34944  ballotlemfp1  34947  ballotlemfval0  34951  chtvalz  35081  dfscott3  35570  fmla0disjsuc  35927  mthmpps  36111  dffv5  36451  bj-sscon  37722  bj-discrmoore  37810  mblfinlem2  38366  ismblfin  38369  mbfposadd  38375  itg2addnclem2  38380  asindmre  38411  abeqin  38961  xrnres  39132  redundeq1  39420  refrelsredund4  39423  dfpetparts2  39679  dfpeters2  39681  diophrw  43548  dnwech  43833  lmhmlnmsplit  43872  rp-fakeuninass  44300  iunrelexp0  44486  nznngen  45084  uzinico2  46335  limsup0  46466  limsupvaluz  46480  sge0sn  47151  31prm  48407