Theorem ineq1i 4162

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  in12  4174  inindi  4180  dfrab3  4265  dfif5  4499  disjpr2  4674  disjtpsn  4676  disjtp2  4677  uniin1  5033  resres  5985  imainrect  6174  predidm  6324  fresaun  6746  fresaunres2  6747  ssenen  9149  hartogslem1  9514  prinfzo0  13754  leiso  14524  f1oun2prg  14988  smumul  16583  setsfun  17263  setsfun0  17264  firest  17517  lsmdisj2r  19812  frgpuplem  19899  ltbwe  22260  tgrest  23384  fiuncmp  23629  ptclsg  23841  metnrmlem3  25088  mbfid  25863  ppi1  27400  cht1  27401  ppiub  27440  lrrecse  28207  lrrecpred  28209  chdmj2i  31963  chjassi  31967  pjoml2i  32066  pjoml4i  32068  cmcmlem  32072  mayetes3i  32210  cvmdi  32805  atomli  32863  atabsi  32882  disjuniel  33070  imadifxp  33074  gtiso  33173  preiman0  33182  nn0disj01  33289  evlextv  34052  prsss  34426  ordtrest2NEW  34433  esumnul  34558  measinblem  34731  eulerpartlemt  34882  ballotlem2  35000  ballotlemfp1  35003  ballotlemfval0  35007  chtvalz  35137  dfscott3  35626  fmla0disjsuc  35977  mthmpps  36161  dffv5  36501  bj-sscon  37773  bj-discrmoore  37861  mblfinlem2  38407  ismblfin  38410  mbfposadd  38416  itg2addnclem2  38421  asindmre  38452  abeqin  39002  xrnres  39173  redundeq1  39461  refrelsredund4  39464  dfpetparts2  39720  dfpeters2  39722  diophrw  43604  dnwech  43889  lmhmlnmsplit  43928  rp-fakeuninass  44356  iunrelexp0  44542  nznngen  45140  uzinico2  46391  limsup0  46522  limsupvaluz  46536  sge0sn  47207  31prm  48500