Theorem ineq2i 4167

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

Syntax hints:   = wceq 1541   ∩ cin 3898

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-in 3906

This theorem is referenced by:  in4  4184  inindir  4186  indif2  4231  difun1  4249  dfrab3ss  4273  undif1  4426  difdifdir  4442  dfif3  4492  dfif5  4494  disjpr2  4668  disjprsn  4669  disjtp2  4671  intunsn  4940  rint0  4941  riin0  5035  csbres  5939  res0  5940  resres  5949  resundi  5950  resindi  5952  inres  5954  resiun2  5957  resopab  5991  dffr3  6056  dfse2  6057  dminxp  6136  imainrect  6137  cnvrescnv  6151  resdmres  6188  resdifdi  6192  dfpo2  6252  snres0  6254  dfpred2  6267  predidm  6282  funimacnv  6571  fresaun  6703  fresaunres2  6704  tfrlem10  8316  sbthlem5  9017  infssuni  9244  dfsup2  9345  en3lplem2  9520  wemapwe  9604  epfrs  9638  r0weon  9920  infxpenlem  9921  kmlem11  10069  ackbij1lem1  10127  ackbij1lem2  10128  axdc3lem4  10361  canthwelem  10559  dmaddpi  10799  dmmulpi  10800  ssxr  11200  dmhashres  14262  fz1isolem  14382  f1oun2prg  14838  fsumiun  15742  sadeq  16397  bitsres  16398  smuval2  16407  smumul  16418  ressinbas  17170  lubdm  18270  glbdm  18283  sylow2a  19546  lsmmod2  19603  lsmdisj2r  19612  ablfac1eu  20002  pjdm  21660  ressmplbas2  21980  opsrtoslem1  22008  rintopn  22851  ordtrest2  23146  cmpsublem  23341  kgentopon  23480  hausdiag  23587  uzrest  23839  ufprim  23851  trust  24171  metnrmlem3  24804  clsocv  25204  ismbl  25481  unmbl  25492  volinun  25501  voliunlem1  25505  ovolioo  25523  itg2cnlem2  25717  ellimc2  25832  limcflf  25836  lhop1lem  25972  lgsquadlem3  27347  rplogsum  27492  noextend  27632  noextendseq  27633  noetasuplem2  27700  noetainflem2  27704  madeval2  27821  onsiso  28236  bdayn0sf1o  28328  umgrislfupgrlem  29144  spthispth  29746  cyclnumvtx  29822  0pth  30149  1pthdlem2  30160  frgrncvvdeqlem3  30325  ex-in  30449  chdmj3i  31507  chdmj4i  31508  chjassi  31510  pjoml2i  31609  pjoml3i  31610  cmcmlem  31615  cmcm2i  31617  cmbr3i  31624  fh3i  31647  fh4i  31648  osumcor2i  31668  mayetes3i  31753  mdslmd3i  32356  mdexchi  32359  atabsi  32425  dmdbr5ati  32446  inin  32540  uniin2  32576  of0r  32707  dfprm3  33583  psrbasfsupp  33642  ordtrest2NEW  34029  hasheuni  34191  carsgclctunlem1  34423  eulerpartgbij  34478  fiblem  34504  cvmscld  35416  sate0  35558  msrid  35688  elrn3  35905  bj-inrab3  37073  poimirlem15  37775  mblfinlem2  37798  ftc1anclem6  37838  dmxrncnvep  38513  dmcnvepres  38514  dmuncnvepres  38515  dmxrnuncnvepres  38516  xrnres2  38550  redundss3  38824  refrelsredund4  38828  pol0N  40108  readvrec2  42558  mapfzcons2  42903  diophrw  42943  conrel2d  43847  iunrelexp0  43885  hashnzfz  44503  wfaxpow  45180  disjinfi  45378  fourierdlem80  46372  sge0resplit  46592  sge0split  46595  caragenuncllem  46698  iscnrm3rlem1  49127