Theorem ineq2i 4144

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

Syntax hints:   = wceq 1539   ∩ cin 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3895

This theorem is referenced by:  in4  4160  inindir  4162  indif2  4205  difun1  4224  dfrab3ss  4247  undif1  4410  difdifdir  4423  dfif3  4474  dfif5  4476  disjpr2  4650  disjprsn  4651  disjtp2  4653  intunsn  4921  rint0  4922  riin0  5012  csbres  5897  res0  5898  resres  5907  resundi  5908  resindi  5910  inres  5912  resiun2  5915  resopab  5945  dffr3  6010  dfse2  6011  dminxp  6088  imainrect  6089  cnvrescnv  6103  resdmres  6140  resdifdi  6144  dfpo2  6203  dfpred2  6216  predidm  6233  funimacnv  6522  fresaun  6654  fresaunres2  6655  wfrlem13OLD  8161  tfrlem10  8227  sbthlem5  8883  infssuni  9119  dfsup2  9212  en3lplem2  9380  wemapwe  9464  epfrs  9498  r0weon  9777  infxpenlem  9778  kmlem11  9925  ackbij1lem1  9985  ackbij1lem2  9986  axdc3lem4  10218  canthwelem  10415  dmaddpi  10655  dmmulpi  10656  ssxr  11053  dmhashres  14064  fz1isolem  14184  f1oun2prg  14639  fsumiun  15542  sadeq  16188  bitsres  16189  smuval2  16198  smumul  16209  ressinbas  16964  lubdm  18078  glbdm  18091  sylow2a  19233  lsmmod2  19291  lsmdisj2r  19300  ablfac1eu  19685  pjdm  20923  ressmplbas2  21237  opsrtoslem1  21271  rintopn  22067  ordtrest2  22364  cmpsublem  22559  kgentopon  22698  hausdiag  22805  uzrest  23057  ufprim  23069  trust  23390  metnrmlem3  24033  clsocv  24423  ismbl  24699  unmbl  24710  volinun  24719  voliunlem1  24723  ovolioo  24741  itg2cnlem2  24936  ellimc2  25050  limcflf  25054  lhop1lem  25186  lgsquadlem3  26539  rplogsum  26684  umgrislfupgrlem  27501  spthispth  28103  0pth  28498  1pthdlem2  28509  frgrncvvdeqlem3  28674  ex-in  28798  chdmj3i  29854  chdmj4i  29855  chjassi  29857  pjoml2i  29956  pjoml3i  29957  cmcmlem  29962  cmcm2i  29964  cmbr3i  29971  fh3i  29994  fh4i  29995  osumcor2i  30015  mayetes3i  30100  mdslmd3i  30703  mdexchi  30706  atabsi  30772  dmdbr5ati  30793  inin  30871  uniin2  30901  ordtrest2NEW  31882  hasheuni  32062  carsgclctunlem1  32293  eulerpartgbij  32348  fiblem  32374  cvmscld  33244  sate0  33386  msrid  33516  snres0  33684  elrn3  33738  noextend  33878  noextendseq  33879  noetasuplem2  33946  noetainflem2  33950  madeval2  34046  bj-inrab3  35126  poimirlem15  35801  mblfinlem2  35824  ftc1anclem6  35864  xrnres2  36536  redundss3  36748  refrelsredund4  36752  pol0N  37930  mapfzcons2  40548  diophrw  40588  conrel2d  41279  iunrelexp0  41317  hashnzfz  41945  disjinfi  42738  fourierdlem80  43734  sge0resplit  43951  sge0split  43954  caragenuncllem  44057  iscnrm3rlem1  46245