Theorem ineq2i 4176

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

Syntax hints:   = wceq 1540   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-in 3918

This theorem is referenced by:  in4  4193  inindir  4195  indif2  4240  difun1  4258  dfrab3ss  4282  undif1  4435  difdifdir  4451  dfif3  4499  dfif5  4501  disjpr2  4673  disjprsn  4674  disjtp2  4676  intunsn  4947  rint0  4948  riin0  5041  csbres  5942  res0  5943  resres  5952  resundi  5953  resindi  5955  inres  5957  resiun2  5960  resopab  5994  dffr3  6059  dfse2  6060  dminxp  6141  imainrect  6142  cnvrescnv  6156  resdmres  6193  resdifdi  6197  dfpo2  6257  snres0  6259  dfpred2  6272  predidm  6287  funimacnv  6581  fresaun  6713  fresaunres2  6714  tfrlem10  8332  sbthlem5  9032  infssuni  9273  dfsup2  9371  en3lplem2  9542  wemapwe  9626  epfrs  9660  r0weon  9941  infxpenlem  9942  kmlem11  10090  ackbij1lem1  10148  ackbij1lem2  10149  axdc3lem4  10382  canthwelem  10579  dmaddpi  10819  dmmulpi  10820  ssxr  11219  dmhashres  14282  fz1isolem  14402  f1oun2prg  14859  fsumiun  15763  sadeq  16418  bitsres  16419  smuval2  16428  smumul  16439  ressinbas  17191  lubdm  18290  glbdm  18303  sylow2a  19533  lsmmod2  19590  lsmdisj2r  19599  ablfac1eu  19989  pjdm  21649  ressmplbas2  21967  opsrtoslem1  21995  rintopn  22829  ordtrest2  23124  cmpsublem  23319  kgentopon  23458  hausdiag  23565  uzrest  23817  ufprim  23829  trust  24150  metnrmlem3  24783  clsocv  25183  ismbl  25460  unmbl  25471  volinun  25480  voliunlem1  25484  ovolioo  25502  itg2cnlem2  25696  ellimc2  25811  limcflf  25815  lhop1lem  25951  lgsquadlem3  27326  rplogsum  27471  noextend  27611  noextendseq  27612  noetasuplem2  27679  noetainflem2  27683  madeval2  27798  onsiso  28209  bdayn0sf1o  28299  umgrislfupgrlem  29102  spthispth  29704  cyclnumvtx  29780  0pth  30104  1pthdlem2  30115  frgrncvvdeqlem3  30280  ex-in  30404  chdmj3i  31462  chdmj4i  31463  chjassi  31465  pjoml2i  31564  pjoml3i  31565  cmcmlem  31570  cmcm2i  31572  cmbr3i  31579  fh3i  31602  fh4i  31603  osumcor2i  31623  mayetes3i  31708  mdslmd3i  32311  mdexchi  32314  atabsi  32380  dmdbr5ati  32401  inin  32495  uniin2  32531  of0r  32652  dfprm3  33517  ordtrest2NEW  33906  hasheuni  34068  carsgclctunlem1  34301  eulerpartgbij  34356  fiblem  34382  cvmscld  35253  sate0  35395  msrid  35525  elrn3  35742  bj-inrab3  36910  poimirlem15  37622  mblfinlem2  37645  ftc1anclem6  37685  dmxrncnvep  38355  xrnres2  38382  redundss3  38612  refrelsredund4  38616  pol0N  39896  readvrec2  42342  mapfzcons2  42700  diophrw  42740  conrel2d  43646  iunrelexp0  43684  hashnzfz  44302  wfaxpow  44980  disjinfi  45179  fourierdlem80  46177  sge0resplit  46397  sge0split  46400  caragenuncllem  46503  iscnrm3rlem1  48921