Theorem ineq2i 4197

Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)

Hypothesis

Ref	Expression
ineq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
ineq2i	⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)

Proof of Theorem ineq2i

Step	Hyp	Ref	Expression
1		ineq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		ineq2 4194	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵)

Syntax hints:   = wceq 1540   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938

This theorem is referenced by:  in4  4214  inindir  4216  indif2  4261  difun1  4279  dfrab3ss  4303  undif1  4456  difdifdir  4472  dfif3  4520  dfif5  4522  disjpr2  4694  disjprsn  4695  disjtp2  4697  intunsn  4968  rint0  4969  riin0  5063  csbres  5974  res0  5975  resres  5984  resundi  5985  resindi  5987  inres  5989  resiun2  5992  resopab  6026  dffr3  6091  dfse2  6092  dminxp  6174  imainrect  6175  cnvrescnv  6189  resdmres  6226  resdifdi  6230  dfpo2  6290  snres0  6292  dfpred2  6305  predidm  6320  funimacnv  6622  fresaun  6754  fresaunres2  6755  wfrlem13OLD  8340  tfrlem10  8406  sbthlem5  9106  infssuni  9363  dfsup2  9461  en3lplem2  9632  wemapwe  9716  epfrs  9750  r0weon  10031  infxpenlem  10032  kmlem11  10180  ackbij1lem1  10238  ackbij1lem2  10239  axdc3lem4  10472  canthwelem  10669  dmaddpi  10909  dmmulpi  10910  ssxr  11309  dmhashres  14364  fz1isolem  14484  f1oun2prg  14941  fsumiun  15842  sadeq  16496  bitsres  16497  smuval2  16506  smumul  16517  ressinbas  17271  lubdm  18366  glbdm  18379  sylow2a  19605  lsmmod2  19662  lsmdisj2r  19671  ablfac1eu  20061  pjdm  21672  ressmplbas2  21990  opsrtoslem1  22018  rintopn  22852  ordtrest2  23147  cmpsublem  23342  kgentopon  23481  hausdiag  23588  uzrest  23840  ufprim  23852  trust  24173  metnrmlem3  24806  clsocv  25207  ismbl  25484  unmbl  25495  volinun  25504  voliunlem1  25508  ovolioo  25526  itg2cnlem2  25720  ellimc2  25835  limcflf  25839  lhop1lem  25975  lgsquadlem3  27350  rplogsum  27495  noextend  27635  noextendseq  27636  noetasuplem2  27703  noetainflem2  27707  madeval2  27818  onsiso  28226  bdayn0sf1o  28316  umgrislfupgrlem  29106  spthispth  29711  cyclnumvtx  29787  0pth  30111  1pthdlem2  30122  frgrncvvdeqlem3  30287  ex-in  30411  chdmj3i  31469  chdmj4i  31470  chjassi  31472  pjoml2i  31571  pjoml3i  31572  cmcmlem  31577  cmcm2i  31579  cmbr3i  31586  fh3i  31609  fh4i  31610  osumcor2i  31630  mayetes3i  31715  mdslmd3i  32318  mdexchi  32321  atabsi  32387  dmdbr5ati  32408  inin  32502  uniin2  32538  of0r  32661  dfprm3  33573  ordtrest2NEW  33959  hasheuni  34121  carsgclctunlem1  34354  eulerpartgbij  34409  fiblem  34435  cvmscld  35300  sate0  35442  msrid  35572  elrn3  35784  bj-inrab3  36952  poimirlem15  37664  mblfinlem2  37687  ftc1anclem6  37727  xrnres2  38426  redundss3  38651  refrelsredund4  38655  pol0N  39933  readvrec2  42379  mapfzcons2  42717  diophrw  42757  conrel2d  43663  iunrelexp0  43701  hashnzfz  44319  wfaxpow  44997  disjinfi  45196  fourierdlem80  46195  sge0resplit  46415  sge0split  46418  caragenuncllem  46521  iscnrm3rlem1  48894