Theorem ineq2i 4110

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

Syntax hints:   = wceq 1543   ∩ cin 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-in 3860

This theorem is referenced by:  in4  4126  inindir  4128  indif2  4171  difun1  4190  dfrab3ss  4213  undif1  4376  difdifdir  4389  dfif3  4439  dfif5  4441  disjpr2  4615  disjprsn  4616  disjtp2  4618  intunsn  4886  rint0  4887  riin0  4976  csbres  5839  res0  5840  resres  5849  resundi  5850  resindi  5852  inres  5854  resiun2  5857  resopab  5887  dffr3  5947  dfse2  5948  dminxp  6023  imainrect  6024  cnvrescnv  6038  resdmres  6075  resdifdi  6079  dfpred2  6149  predidm  6162  funimacnv  6439  fresaun  6568  fresaunres2  6569  wfrlem13  8045  tfrlem10  8101  sbthlem5  8738  infssuni  8945  dfsup2  9038  en3lplem2  9206  wemapwe  9290  epfrs  9325  r0weon  9591  infxpenlem  9592  kmlem11  9739  ackbij1lem1  9799  ackbij1lem2  9800  axdc3lem4  10032  canthwelem  10229  dmaddpi  10469  dmmulpi  10470  ssxr  10867  dmhashres  13872  fz1isolem  13992  f1oun2prg  14447  fsumiun  15348  sadeq  15994  bitsres  15995  smuval2  16004  smumul  16015  ressinbas  16744  lubdm  17811  glbdm  17824  sylow2a  18962  lsmmod2  19020  lsmdisj2r  19029  ablfac1eu  19414  pjdm  20623  ressmplbas2  20938  opsrtoslem1  20966  rintopn  21760  ordtrest2  22055  cmpsublem  22250  kgentopon  22389  hausdiag  22496  uzrest  22748  ufprim  22760  trust  23081  metnrmlem3  23712  clsocv  24101  ismbl  24377  unmbl  24388  volinun  24397  voliunlem1  24401  ovolioo  24419  itg2cnlem2  24614  ellimc2  24728  limcflf  24732  lhop1lem  24864  lgsquadlem3  26217  rplogsum  26362  umgrislfupgrlem  27167  spthispth  27767  0pth  28162  1pthdlem2  28173  frgrncvvdeqlem3  28338  ex-in  28462  chdmj3i  29518  chdmj4i  29519  chjassi  29521  pjoml2i  29620  pjoml3i  29621  cmcmlem  29626  cmcm2i  29628  cmbr3i  29635  fh3i  29658  fh4i  29659  osumcor2i  29679  mayetes3i  29764  mdslmd3i  30367  mdexchi  30370  atabsi  30436  dmdbr5ati  30457  inin  30535  uniin2  30565  ordtrest2NEW  31541  hasheuni  31719  carsgclctunlem1  31950  eulerpartgbij  32005  fiblem  32031  cvmscld  32902  sate0  33044  msrid  33174  snres0  33344  dfpo2  33392  elrn3  33399  noextend  33555  noextendseq  33556  noetasuplem2  33623  noetainflem2  33627  madeval2  33723  bj-inrab3  34803  poimirlem15  35478  mblfinlem2  35501  ftc1anclem6  35541  xrnres2  36215  redundss3  36427  refrelsredund4  36431  pol0N  37609  mapfzcons2  40185  diophrw  40225  conrel2d  40890  iunrelexp0  40928  hashnzfz  41552  disjinfi  42345  fourierdlem80  43345  sge0resplit  43562  sge0split  43565  caragenuncllem  43668  iscnrm3rlem1  45850