Theorem ineq2i 4140

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

Syntax hints:   = wceq 1539   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890

This theorem is referenced by:  in4  4156  inindir  4158  indif2  4201  difun1  4220  dfrab3ss  4243  undif1  4406  difdifdir  4419  dfif3  4470  dfif5  4472  disjpr2  4646  disjprsn  4647  disjtp2  4649  intunsn  4917  rint0  4918  riin0  5007  csbres  5883  res0  5884  resres  5893  resundi  5894  resindi  5896  inres  5898  resiun2  5901  resopab  5931  dffr3  5996  dfse2  5997  dminxp  6072  imainrect  6073  cnvrescnv  6087  resdmres  6124  resdifdi  6128  dfpo2  6188  dfpred2  6201  predidm  6218  funimacnv  6499  fresaun  6629  fresaunres2  6630  wfrlem13OLD  8123  tfrlem10  8189  sbthlem5  8827  infssuni  9040  dfsup2  9133  en3lplem2  9301  wemapwe  9385  epfrs  9420  r0weon  9699  infxpenlem  9700  kmlem11  9847  ackbij1lem1  9907  ackbij1lem2  9908  axdc3lem4  10140  canthwelem  10337  dmaddpi  10577  dmmulpi  10578  ssxr  10975  dmhashres  13983  fz1isolem  14103  f1oun2prg  14558  fsumiun  15461  sadeq  16107  bitsres  16108  smuval2  16117  smumul  16128  ressinbas  16881  lubdm  17984  glbdm  17997  sylow2a  19139  lsmmod2  19197  lsmdisj2r  19206  ablfac1eu  19591  pjdm  20824  ressmplbas2  21138  opsrtoslem1  21172  rintopn  21966  ordtrest2  22263  cmpsublem  22458  kgentopon  22597  hausdiag  22704  uzrest  22956  ufprim  22968  trust  23289  metnrmlem3  23930  clsocv  24319  ismbl  24595  unmbl  24606  volinun  24615  voliunlem1  24619  ovolioo  24637  itg2cnlem2  24832  ellimc2  24946  limcflf  24950  lhop1lem  25082  lgsquadlem3  26435  rplogsum  26580  umgrislfupgrlem  27395  spthispth  27995  0pth  28390  1pthdlem2  28401  frgrncvvdeqlem3  28566  ex-in  28690  chdmj3i  29746  chdmj4i  29747  chjassi  29749  pjoml2i  29848  pjoml3i  29849  cmcmlem  29854  cmcm2i  29856  cmbr3i  29863  fh3i  29886  fh4i  29887  osumcor2i  29907  mayetes3i  29992  mdslmd3i  30595  mdexchi  30598  atabsi  30664  dmdbr5ati  30685  inin  30763  uniin2  30793  ordtrest2NEW  31775  hasheuni  31953  carsgclctunlem1  32184  eulerpartgbij  32239  fiblem  32265  cvmscld  33135  sate0  33277  msrid  33407  snres0  33577  elrn3  33635  noextend  33796  noextendseq  33797  noetasuplem2  33864  noetainflem2  33868  madeval2  33964  bj-inrab3  35044  poimirlem15  35719  mblfinlem2  35742  ftc1anclem6  35782  xrnres2  36456  redundss3  36668  refrelsredund4  36672  pol0N  37850  mapfzcons2  40457  diophrw  40497  conrel2d  41161  iunrelexp0  41199  hashnzfz  41827  disjinfi  42620  fourierdlem80  43617  sge0resplit  43834  sge0split  43837  caragenuncllem  43940  iscnrm3rlem1  46122