Theorem ineq1i 4200

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

Syntax hints:   = wceq 1533   ∩ cin 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-in 3947

This theorem is referenced by:  in12  4212  inindi  4218  dfrab3  4301  dfif5  4536  disjpr2  4709  disjtpsn  4711  disjtp2  4712  resres  5984  imainrect  6170  predidm  6317  fresaun  6752  fresaunres2  6753  ssenen  9146  hartogslem1  9532  prinfzo0  13667  leiso  14416  f1oun2prg  14864  smumul  16430  setsfun  17100  setsfun0  17101  firest  17374  lsmdisj2r  19590  frgpuplem  19677  ltbwe  21900  tgrest  22973  fiuncmp  23218  ptclsg  23429  metnrmlem3  24687  mbfid  25474  ppi1  27000  cht1  27001  ppiub  27041  lrrecse  27763  lrrecpred  27765  chdmj2i  31159  chjassi  31163  pjoml2i  31262  pjoml4i  31264  cmcmlem  31268  mayetes3i  31406  cvmdi  32001  atomli  32059  atabsi  32078  uniin1  32207  disjuniel  32252  imadifxp  32256  gtiso  32346  preiman0  32355  prsss  33351  ordtrest2NEW  33358  esumnul  33501  measinblem  33673  eulerpartlemt  33825  ballotlem2  33942  ballotlemfp1  33945  ballotlemfval0  33949  chtvalz  34096  fmla0disjsuc  34844  mthmpps  35028  dffv5  35357  bj-sscon  36366  bj-discrmoore  36448  mblfinlem2  36982  ismblfin  36985  mbfposadd  36991  itg2addnclem2  36996  asindmre  37027  abeqin  37576  xrnres  37728  redundeq1  37955  refrelsredund4  37958  diophrw  41952  dnwech  42245  lmhmlnmsplit  42284  rp-fakeuninass  42722  iunrelexp0  42908  nznngen  43530  uzinico2  44726  limsup0  44861  limsupvaluz  44875  sge0sn  45546  31prm  46716