Theorem ineq1i 4009

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

Syntax hints:   = wceq 1637   ∩ cin 3768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776

This theorem is referenced by:  in12  4021  inindi  4027  dfrab3  4103  dfif5  4295  disjpr2  4440  disjtpsn  4442  disjtp2  4443  resres  5613  imainrect  5786  predidm  5915  fresaun  6290  fresaunres2  6291  ssenen  8373  hartogslem1  8686  prinfzo0  12731  leiso  13460  f1oun2prg  13886  smumul  15434  setsfun  16104  setsfun0  16105  firest  16298  lsmdisj2r  18299  frgpuplem  18386  ltbwe  19681  tgrest  21177  fiuncmp  21421  ptclsg  21632  metnrmlem3  22877  mbfid  23616  ppi1  25104  cht1  25105  ppiub  25143  chdmj2i  28669  chjassi  28673  pjoml2i  28772  pjoml4i  28774  cmcmlem  28778  mayetes3i  28916  cvmdi  29511  atomli  29569  atabsi  29588  uniin1  29692  disjuniel  29735  imadifxp  29739  gtiso  29805  prsss  30287  ordtrest2NEW  30294  esumnul  30435  measinblem  30608  eulerpartlemt  30758  ballotlem2  30875  ballotlemfp1  30878  ballotlemfval0  30882  chtvalz  31032  mthmpps  31802  dffv5  32352  bj-sscon  33324  bj-discrmoore  33377  mblfinlem2  33760  ismblfin  33763  mbfposadd  33769  itg2addnclem2  33774  asindmre  33807  abeqin  34335  xrnres  34473  diophrw  37824  dnwech  38119  lmhmlnmsplit  38158  rp-fakeuninass  38362  iunrelexp0  38494  nznngen  39015  uzinico2  40269  limsup0  40406  limsupvaluz  40420  sge0sn  41075  31prm  42087