Theorem ineq2i 4209

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

Syntax hints:   = wceq 1542   ∩ cin 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3955

This theorem is referenced by:  in4  4225  inindir  4227  indif2  4270  difun1  4289  dfrab3ss  4312  undif1  4475  difdifdir  4491  dfif3  4542  dfif5  4544  disjpr2  4717  disjprsn  4718  disjtp2  4720  intunsn  4993  rint0  4994  riin0  5085  csbres  5983  res0  5984  resres  5993  resundi  5994  resindi  5996  inres  5998  resiun2  6001  resopab  6033  dffr3  6096  dfse2  6097  dminxp  6177  imainrect  6178  cnvrescnv  6192  resdmres  6229  resdifdi  6233  dfpo2  6293  snres0  6295  dfpred2  6308  predidm  6325  funimacnv  6627  fresaun  6760  fresaunres2  6761  wfrlem13OLD  8318  tfrlem10  8384  sbthlem5  9084  infssuni  9340  dfsup2  9436  en3lplem2  9605  wemapwe  9689  epfrs  9723  r0weon  10004  infxpenlem  10005  kmlem11  10152  ackbij1lem1  10212  ackbij1lem2  10213  axdc3lem4  10445  canthwelem  10642  dmaddpi  10882  dmmulpi  10883  ssxr  11280  dmhashres  14298  fz1isolem  14419  f1oun2prg  14865  fsumiun  15764  sadeq  16410  bitsres  16411  smuval2  16420  smumul  16431  ressinbas  17187  lubdm  18301  glbdm  18314  sylow2a  19482  lsmmod2  19539  lsmdisj2r  19548  ablfac1eu  19938  pjdm  21254  ressmplbas2  21574  opsrtoslem1  21608  rintopn  22403  ordtrest2  22700  cmpsublem  22895  kgentopon  23034  hausdiag  23141  uzrest  23393  ufprim  23405  trust  23726  metnrmlem3  24369  clsocv  24759  ismbl  25035  unmbl  25046  volinun  25055  voliunlem1  25059  ovolioo  25077  itg2cnlem2  25272  ellimc2  25386  limcflf  25390  lhop1lem  25522  lgsquadlem3  26875  rplogsum  27020  noextend  27159  noextendseq  27160  noetasuplem2  27227  noetainflem2  27231  madeval2  27338  umgrislfupgrlem  28372  spthispth  28973  0pth  29368  1pthdlem2  29379  frgrncvvdeqlem3  29544  ex-in  29668  chdmj3i  30724  chdmj4i  30725  chjassi  30727  pjoml2i  30826  pjoml3i  30827  cmcmlem  30832  cmcm2i  30834  cmbr3i  30841  fh3i  30864  fh4i  30865  osumcor2i  30885  mayetes3i  30970  mdslmd3i  31573  mdexchi  31576  atabsi  31642  dmdbr5ati  31663  inin  31741  uniin2  31772  ordtrest2NEW  32892  hasheuni  33072  carsgclctunlem1  33305  eulerpartgbij  33360  fiblem  33386  cvmscld  34253  sate0  34395  msrid  34525  elrn3  34721  bj-inrab3  35798  poimirlem15  36492  mblfinlem2  36515  ftc1anclem6  36555  xrnres2  37262  redundss3  37487  refrelsredund4  37491  pol0N  38769  mapfzcons2  41443  diophrw  41483  conrel2d  42401  iunrelexp0  42439  hashnzfz  43065  disjinfi  43877  fourierdlem80  44889  sge0resplit  45109  sge0split  45112  caragenuncllem  45215  iscnrm3rlem1  47527