Theorem ineq2i 4017

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

Syntax hints:   = wceq 1637   ∩ cin 3775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-in 3783

This theorem is referenced by:  in4  4033  inindir  4035  indif2  4079  difun1  4096  dfrab3ss  4113  undif1  4246  difdifdir  4259  dfif3  4300  dfif5  4302  disjpr2  4447  disjprsn  4448  disjtp2  4450  intunsn  4715  rint0  4716  riin0  4793  csbres  5607  res0  5608  resres  5620  resundi  5621  resindi  5623  inres  5625  resiun2  5628  resopab  5658  dffr3  5715  dfse2  5716  dminxp  5792  imainrect  5793  resdmres  5846  dfpred2  5909  predidm  5922  funimacnv  6184  fresaun  6293  fresaunres2  6294  wfrlem13  7666  tfrlem10  7722  sbthlem5  8316  infssuni  8499  dfsup2  8592  en3lplem2  8758  wemapwe  8844  epfrs  8857  r0weon  9121  infxpenlem  9122  kmlem11  9270  ackbij1lem1  9330  ackbij1lem2  9331  axdc3lem4  9563  canthwelem  9760  dmaddpi  10000  dmmulpi  10001  ssxr  10395  dmhashres  13352  fz1isolem  13465  f1oun2prg  13889  fsumiun  14778  sadeq  15416  bitsres  15417  smuval2  15426  smumul  15437  ressinbas  16150  lubdm  17187  glbdm  17200  sylow2a  18238  lsmmod2  18293  lsmdisj2r  18302  ablfac1eu  18677  ressmplbas2  19667  opsrtoslem1  19695  pjdm  20265  rintopn  20931  ordtrest2  21226  cmpsublem  21420  kgentopon  21559  hausdiag  21666  uzrest  21918  ufprim  21930  trust  22250  metnrmlem3  22881  clsocv  23265  ismbl  23513  unmbl  23524  volinun  23533  voliunlem1  23537  ovolioo  23555  itg2cnlem2  23749  ellimc2  23861  limcflf  23865  lhop1lem  23996  lgsquadlem3  25327  rplogsum  25436  umgrislfupgrlem  26237  spthispth  26856  0pth  27304  1pthdlem2  27315  frgrncvvdeqlem3  27482  ex-in  27619  chdmj3i  28676  chdmj4i  28677  chjassi  28679  pjoml2i  28778  pjoml3i  28779  cmcmlem  28784  cmcm2i  28786  cmbr3i  28793  fh3i  28816  fh4i  28817  osumcor2i  28837  mayetes3i  28922  mdslmd3i  29525  mdexchi  29528  atabsi  29594  dmdbr5ati  29615  inin  29683  uniin2  29699  ordtrest2NEW  30300  hasheuni  30478  carsgclctunlem1  30710  eulerpartgbij  30765  fiblem  30791  cvmscld  31583  msrid  31770  dfpo2  31972  elrn3  31979  noextend  32145  noextendseq  32146  madeval2  32262  bj-inrab3  33238  poimirlem15  33739  mblfinlem2  33762  ftc1anclem6  33804  xrnres2  34476  pol0N  35691  mapfzcons2  37785  diophrw  37825  conrel2d  38457  iunrelexp0  38495  hashnzfz  39020  disjinfi  39870  fourierdlem80  40883  sge0resplit  41103  sge0split  41106  caragenuncllem  41209