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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  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  5983  imainrect  6173  predidm  6328  fresaun  6751  fresaunres2  6752  ssenen  9163  hartogslem1  9529  prinfzo0  13826  leiso  14597  f1oun2prg  15061  smumul  16656  setsfun  17342  setsfun0  17343  firest  17596  lsmdisj2r  19892  frgpuplem  19979  ltbwe  22346  tgrest  23470  fiuncmp  23715  ptclsg  23927  metnrmlem3  25174  mbfid  25949  ppi1  27484  cht1  27485  ppiub  27524  lrrecse  28321  lrrecpred  28323  chdmj2i  32077  chjassi  32081  pjoml2i  32180  pjoml4i  32182  cmcmlem  32186  mayetes3i  32324  cvmdi  32919  atomli  32977  atabsi  32996  disjuniel  33184  imadifxp  33188  gtiso  33287  preiman0  33296  nn0disj01  33403  evlextv  34167  prsss  34541  ordtrest2NEW  34548  esumnul  34673  measinblem  34846  eulerpartlemt  34996  ballotlem2  35114  ballotlemfp1  35117  ballotlemfval0  35121  chtvalz  35251  dfscott3  35731  fmla0disjsuc  36142  mthmpps  36326  dffv5  36666  bj-sscon  37922  bj-discrmoore  38012  mblfinlem2  38556  ismblfin  38559  mbfposadd  38565  itg2addnclem2  38570  asindmre  38601  abeqin  39166  xrnres  39337  redundeq1  39625  refrelsredund4  39628  dfpetparts2  39884  dfpeters2  39886  diophrw  43749  dnwech  44034  lmhmlnmsplit  44073  rp-fakeuninass  44501  iunrelexp0  44687  nznngen  45285  uzinico2  46542  limsup0  46673  limsupvaluz  46687  sge0sn  47358  31prm  48651