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 1533   ∩ cin 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-in 3953

This theorem is referenced by:  in4  4226  inindir  4228  indif2  4271  difun1  4290  dfrab3ss  4314  undif1  4479  difdifdir  4495  dfif3  4546  dfif5  4548  disjpr2  4721  disjprsn  4722  disjtp2  4724  intunsn  4996  rint0  4997  riin0  5089  csbres  5991  res0  5992  resres  6001  resundi  6002  resindi  6004  inres  6006  resiun2  6009  resopab  6042  dffr3  6108  dfse2  6109  dminxp  6190  imainrect  6191  cnvrescnv  6205  resdmres  6242  resdifdi  6246  dfpo2  6306  snres0  6308  dfpred2  6321  predidm  6338  funimacnv  6639  fresaun  6772  fresaunres2  6773  wfrlem13OLD  8350  tfrlem10  8416  sbthlem5  9124  infssuni  9383  dfsup2  9483  en3lplem2  9652  wemapwe  9736  epfrs  9770  r0weon  10051  infxpenlem  10052  kmlem11  10199  ackbij1lem1  10259  ackbij1lem2  10260  axdc3lem4  10492  canthwelem  10689  dmaddpi  10929  dmmulpi  10930  ssxr  11329  dmhashres  14353  fz1isolem  14475  f1oun2prg  14921  fsumiun  15820  sadeq  16467  bitsres  16468  smuval2  16477  smumul  16488  ressinbas  17254  lubdm  18371  glbdm  18384  sylow2a  19612  lsmmod2  19669  lsmdisj2r  19678  ablfac1eu  20068  pjdm  21697  ressmplbas2  22026  opsrtoslem1  22060  rintopn  22894  ordtrest2  23191  cmpsublem  23386  kgentopon  23525  hausdiag  23632  uzrest  23884  ufprim  23896  trust  24217  metnrmlem3  24860  clsocv  25261  ismbl  25538  unmbl  25549  volinun  25558  voliunlem1  25562  ovolioo  25580  itg2cnlem2  25775  ellimc2  25889  limcflf  25893  lhop1lem  26029  lgsquadlem3  27403  rplogsum  27548  noextend  27688  noextendseq  27689  noetasuplem2  27756  noetainflem2  27760  madeval2  27869  umgrislfupgrlem  29050  spthispth  29655  0pth  30050  1pthdlem2  30061  frgrncvvdeqlem3  30226  ex-in  30350  chdmj3i  31408  chdmj4i  31409  chjassi  31411  pjoml2i  31510  pjoml3i  31511  cmcmlem  31516  cmcm2i  31518  cmbr3i  31525  fh3i  31548  fh4i  31549  osumcor2i  31569  mayetes3i  31654  mdslmd3i  32257  mdexchi  32260  atabsi  32326  dmdbr5ati  32347  inin  32433  uniin2  32464  of0r  32587  dfprm3  33405  ordtrest2NEW  33694  hasheuni  33874  carsgclctunlem1  34107  eulerpartgbij  34162  fiblem  34188  cvmscld  35053  sate0  35195  msrid  35325  elrn3  35532  bj-inrab3  36583  poimirlem15  37284  mblfinlem2  37307  ftc1anclem6  37347  xrnres2  38049  redundss3  38274  refrelsredund4  38278  pol0N  39556  mapfzcons2  42313  diophrw  42353  conrel2d  43268  iunrelexp0  43306  hashnzfz  43931  disjinfi  44736  fourierdlem80  45744  sge0resplit  45964  sge0split  45967  caragenuncllem  46070  iscnrm3rlem1  48211