Theorem ineq2i 4169

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

Syntax hints:   = wceq 1541   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908

This theorem is referenced by:  in4  4186  inindir  4188  indif2  4233  difun1  4251  dfrab3ss  4275  undif1  4428  difdifdir  4444  dfif3  4494  dfif5  4496  disjpr2  4670  disjprsn  4671  disjtp2  4673  intunsn  4942  rint0  4943  riin0  5037  csbres  5941  res0  5942  resres  5951  resundi  5952  resindi  5954  inres  5956  resiun2  5959  resopab  5993  dffr3  6058  dfse2  6059  dminxp  6138  imainrect  6139  cnvrescnv  6153  resdmres  6190  resdifdi  6194  dfpo2  6254  snres0  6256  dfpred2  6269  predidm  6284  funimacnv  6573  fresaun  6705  fresaunres2  6706  tfrlem10  8318  sbthlem5  9019  infssuni  9246  dfsup2  9347  en3lplem2  9522  wemapwe  9606  epfrs  9640  r0weon  9922  infxpenlem  9923  kmlem11  10071  ackbij1lem1  10129  ackbij1lem2  10130  axdc3lem4  10363  canthwelem  10561  dmaddpi  10801  dmmulpi  10802  ssxr  11202  dmhashres  14264  fz1isolem  14384  f1oun2prg  14840  fsumiun  15744  sadeq  16399  bitsres  16400  smuval2  16409  smumul  16420  ressinbas  17172  lubdm  18272  glbdm  18285  sylow2a  19548  lsmmod2  19605  lsmdisj2r  19614  ablfac1eu  20004  pjdm  21662  ressmplbas2  21982  opsrtoslem1  22010  rintopn  22853  ordtrest2  23148  cmpsublem  23343  kgentopon  23482  hausdiag  23589  uzrest  23841  ufprim  23853  trust  24173  metnrmlem3  24806  clsocv  25206  ismbl  25483  unmbl  25494  volinun  25503  voliunlem1  25507  ovolioo  25525  itg2cnlem2  25719  ellimc2  25834  limcflf  25838  lhop1lem  25974  lgsquadlem3  27349  rplogsum  27494  noextend  27634  noextendseq  27635  noetasuplem2  27702  noetainflem2  27706  madeval2  27829  oniso  28267  bdayn0sf1o  28366  umgrislfupgrlem  29195  spthispth  29797  cyclnumvtx  29873  0pth  30200  1pthdlem2  30211  frgrncvvdeqlem3  30376  ex-in  30500  chdmj3i  31558  chdmj4i  31559  chjassi  31561  pjoml2i  31660  pjoml3i  31661  cmcmlem  31666  cmcm2i  31668  cmbr3i  31675  fh3i  31698  fh4i  31699  osumcor2i  31719  mayetes3i  31804  mdslmd3i  32407  mdexchi  32410  atabsi  32476  dmdbr5ati  32497  inin  32591  uniin2  32627  of0r  32758  dfprm3  33634  psrbasfsupp  33693  ordtrest2NEW  34080  hasheuni  34242  carsgclctunlem1  34474  eulerpartgbij  34529  fiblem  34555  cvmscld  35467  sate0  35609  msrid  35739  elrn3  35956  bj-inrab3  37130  poimirlem15  37836  mblfinlem2  37859  ftc1anclem6  37899  dmxrncnvep  38584  dmcnvepres  38585  dmuncnvepres  38586  dmxrnuncnvepres  38587  xrnres2  38621  redundss3  38895  refrelsredund4  38899  pol0N  40179  readvrec2  42626  mapfzcons2  42971  diophrw  43011  conrel2d  43915  iunrelexp0  43953  hashnzfz  44571  wfaxpow  45248  disjinfi  45446  fourierdlem80  46440  sge0resplit  46660  sge0split  46663  caragenuncllem  46766  iscnrm3rlem1  49195