Theorem ineq1i 4179

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

Syntax hints:   = wceq 1540   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921

This theorem is referenced by:  in12  4192  inindi  4198  dfrab3  4282  dfif5  4505  disjpr2  4677  disjtpsn  4679  disjtp2  4680  resres  5963  imainrect  6154  predidm  6299  fresaun  6731  fresaunres2  6732  ssenen  9115  hartogslem1  9495  prinfzo0  13659  leiso  14424  f1oun2prg  14883  smumul  16463  setsfun  17141  setsfun0  17142  firest  17395  lsmdisj2r  19615  frgpuplem  19702  ltbwe  21951  tgrest  23046  fiuncmp  23291  ptclsg  23502  metnrmlem3  24750  mbfid  25536  ppi1  27074  cht1  27075  ppiub  27115  lrrecse  27849  lrrecpred  27851  chdmj2i  31411  chjassi  31415  pjoml2i  31514  pjoml4i  31516  cmcmlem  31520  mayetes3i  31658  cvmdi  32253  atomli  32311  atabsi  32330  uniin1  32480  disjuniel  32526  imadifxp  32530  gtiso  32624  preiman0  32633  nn0disj01  32743  prsss  33906  ordtrest2NEW  33913  esumnul  34038  measinblem  34210  eulerpartlemt  34362  ballotlem2  34480  ballotlemfp1  34483  ballotlemfval0  34487  chtvalz  34620  fmla0disjsuc  35385  mthmpps  35569  dffv5  35912  bj-sscon  37017  bj-discrmoore  37099  mblfinlem2  37652  ismblfin  37655  mbfposadd  37661  itg2addnclem2  37666  asindmre  37697  abeqin  38241  xrnres  38388  redundeq1  38620  refrelsredund4  38623  diophrw  42747  dnwech  43037  lmhmlnmsplit  43076  rp-fakeuninass  43505  iunrelexp0  43691  nznngen  44305  uzinico2  45559  limsup0  45692  limsupvaluz  45706  sge0sn  46377  31prm  47595