Theorem ineq1i 4185

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

Syntax hints:   = wceq 1537   ∩ cin 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3943

This theorem is referenced by:  in12  4197  inindi  4203  dfrab3  4278  dfif5  4483  disjpr2  4649  disjtpsn  4651  disjtp2  4652  resres  5866  imainrect  6038  predidm  6170  fresaun  6549  fresaunres2  6550  ssenen  8691  hartogslem1  9006  prinfzo0  13077  leiso  13818  f1oun2prg  14279  smumul  15842  setsfun  16518  setsfun0  16519  firest  16706  lsmdisj2r  18811  frgpuplem  18898  ltbwe  20253  tgrest  21767  fiuncmp  22012  ptclsg  22223  metnrmlem3  23469  mbfid  24236  ppi1  25741  cht1  25742  ppiub  25780  chdmj2i  29259  chjassi  29263  pjoml2i  29362  pjoml4i  29364  cmcmlem  29368  mayetes3i  29506  cvmdi  30101  atomli  30159  atabsi  30178  uniin1  30303  disjuniel  30347  imadifxp  30351  gtiso  30436  prsss  31159  ordtrest2NEW  31166  esumnul  31307  measinblem  31479  eulerpartlemt  31629  ballotlem2  31746  ballotlemfp1  31749  ballotlemfval0  31753  chtvalz  31900  fmla0disjsuc  32645  mthmpps  32829  dffv5  33385  bj-sscon  34344  bj-discrmoore  34406  mblfinlem2  34945  ismblfin  34948  mbfposadd  34954  itg2addnclem2  34959  asindmre  34992  abeqin  35529  xrnres  35665  redundeq1  35879  refrelsredund4  35882  diophrw  39405  dnwech  39697  lmhmlnmsplit  39736  rp-fakeuninass  39931  iunrelexp0  40096  nznngen  40697  uzinico2  41887  limsup0  42024  limsupvaluz  42038  sge0sn  42710  31prm  43809