Theorem ineq1i 4145

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

Syntax hints:   = wceq 1547   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-in 3890

This theorem is referenced by:  in12  4157  inindi  4163  dfrab3  4247  dfif5  4471  disjpr2  4645  disjtpsn  4647  disjtp2  4648  resres  5944  imainrect  6132  predidm  6277  fresaun  6698  fresaunres2  6699  ssenen  9079  hartogslem1  9447  prinfzo0  13644  leiso  14412  f1oun2prg  14870  smumul  16453  setsfun  17132  setsfun0  17133  firest  17386  lsmdisj2r  19651  frgpuplem  19738  ltbwe  22020  tgrest  23142  fiuncmp  23387  ptclsg  23598  metnrmlem3  24845  mbfid  25620  ppi1  27145  cht1  27146  ppiub  27185  lrrecse  27952  lrrecpred  27954  chdmj2i  31571  chjassi  31575  pjoml2i  31674  pjoml4i  31676  cmcmlem  31680  mayetes3i  31818  cvmdi  32413  atomli  32471  atabsi  32490  uniin1  32640  disjuniel  32686  imadifxp  32690  gtiso  32793  preiman0  32802  nn0disj01  32911  evlextv  33726  esplyind  33759  prsss  34100  ordtrest2NEW  34107  esumnul  34232  measinblem  34404  eulerpartlemt  34555  ballotlem2  34673  ballotlemfp1  34676  ballotlemfval0  34680  chtvalz  34813  fmla0disjsuc  35626  mthmpps  35810  dffv5  36150  bj-sscon  37382  bj-discrmoore  37469  mblfinlem2  38025  ismblfin  38028  mbfposadd  38034  itg2addnclem2  38039  asindmre  38070  abeqin  38621  xrnres  38792  redundeq1  39080  refrelsredund4  39083  dfpetparts2  39339  dfpeters2  39341  diophrw  43208  dnwech  43493  lmhmlnmsplit  43532  rp-fakeuninass  43960  iunrelexp0  44146  nznngen  44760  uzinico2  46006  limsup0  46137  limsupvaluz  46151  sge0sn  46822  31prm  48075