Theorem ineq2i 4163

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

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906

This theorem is used by:  in4  4179  inindir  4181  indif2  4227  difun1  4245  dfrab3ss  4269  undif1  4430  difdifdir  4447  dfif3  4497  dfif5  4499  disjpr2  4674  disjprsn  4675  disjtp2  4677  intunsn  4947  rint0  4948  uniin2  5034  riin0  5042  csbres  5973  res0  5974  resres  5983  resundi  5984  resindi  5986  inres  5988  resiun2  5991  resopab  6026  dffr3  6097  dfse2  6098  dminxp  6172  imainrect  6173  cnvrescnv  6188  resdmres  6233  resdifdi  6237  dfpo2  6299  snres0  6301  dfpred2  6314  predidm  6329  funimacnv  6621  fresaun  6753  fresaunres2  6754  tfrlem10  8395  sbthlem5  9110  infssuni  9335  dfsup2  9436  en3lplem2  9614  wemapwe  9698  epfrs  9732  r0weon  10091  infxpenlem  10092  kmlem11  10239  ackbij1lem1  10297  ackbij1lem2  10298  axdc3lem4  10531  canthwelem  10735  dmaddpi  10975  dmmulpi  10976  ssxr  11379  dmhashres  14485  fz1isolem  14606  f1oun2prg  15068  fsumiun  15988  sadeq  16642  bitsres  16643  smuval2  16652  smumul  16663  ressinbas  17423  lubdm  18523  glbdm  18536  sylow2a  19833  lsmmod2  19890  lsmdisj2r  19899  ablfac1eu  20289  pjdm  22013  ressmplbas2  22335  opsrtoslem1  22364  rintopn  23227  ordtrest2  23522  cmpsublem  23717  kgentopon  23857  hausdiag  23964  uzrest  24216  ufprim  24228  trust  24548  metnrmlem3  25181  clsocv  25571  ismbl  25847  unmbl  25858  volinun  25867  voliunlem1  25871  ovolioo  25889  itg2cnlem2  26083  ellimc2  26197  limcflf  26201  lhop1lem  26333  lgsquadlem3  27709  rplogsum  27854  noextend  28023  noextendseq  28024  noetasuplem2  28091  noetainflem2  28095  madeval2  28219  oniso  28657  bdayn0sf1o  28756  umgrislfupgrlem  29700  spthispth  30309  cyclnumvtx  30388  0pth  30716  1pthdlem2  30727  frgrncvvdeqlem3  30902  ex-in  31026  chdmj3i  32085  chdmj4i  32086  chjassi  32088  pjoml2i  32187  pjoml3i  32188  cmcmlem  32193  cmcm2i  32195  cmbr3i  32202  fh3i  32225  fh4i  32226  osumcor2i  32246  mayetes3i  32331  mdslmd3i  32934  mdexchi  32937  atabsi  33003  dmdbr5ati  33024  inin  33112  of0r  33273  dfprm3  34085  psrbasfsupp  34143  selvply1rhmlemb  34151  ordtrest2NEW  34555  hasheuni  34717  carsgclctunlem1  34949  eulerpartgbij  35004  fiblem  35030  cvmscld  36038  sate0  36180  msrid  36310  elrn3  36527  bj-inrab3  37842  poimirlem15  38553  mblfinlem2  38576  ftc1anclem6  38616  dmxrncnvep  39321  dmcnvepres  39322  dmuncnvepres  39323  dmxrnuncnvepres  39324  xrnres2  39358  redundss3  39644  refrelsredund4  39648  dfpetparts2  39904  dfpeters2  39906  pol0N  40966  readvrec2  43412  mapfzcons2  43729  diophrw  43769  conrel2d  44663  iunrelexp0  44701  hashnzfz  45303  wfaxpow  45986  disjinfi  46206  fourierdlem80  47195  sge0resplit  47415  sge0split  47418  caragenuncllem  47521  iscnrm3rlem1  50047