Theorem ineq2i 4188

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

Syntax hints:   = wceq 1537   ∩ cin 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149  df-in 3945

This theorem is referenced by:  in4  4204  inindir  4206  indif2  4249  difun1  4266  dfrab3ss  4283  undif1  4426  difdifdir  4439  dfif3  4483  dfif5  4485  disjpr2  4651  disjprsn  4652  disjtp2  4654  intunsn  4917  rint0  4918  riin0  5006  csbres  5858  res0  5859  resres  5868  resundi  5869  resindi  5871  inres  5873  resiun2  5876  resopab  5904  dffr3  5964  dfse2  5965  dminxp  6039  imainrect  6040  cnvrescnv  6054  resdmres  6091  dfpred2  6159  predidm  6172  funimacnv  6437  fresaun  6551  fresaunres2  6552  wfrlem13  7969  tfrlem10  8025  sbthlem5  8633  infssuni  8817  dfsup2  8910  en3lplem2  9078  wemapwe  9162  epfrs  9175  r0weon  9440  infxpenlem  9441  kmlem11  9588  ackbij1lem1  9644  ackbij1lem2  9645  axdc3lem4  9877  canthwelem  10074  dmaddpi  10314  dmmulpi  10315  ssxr  10712  dmhashres  13704  fz1isolem  13822  f1oun2prg  14281  fsumiun  15178  sadeq  15823  bitsres  15824  smuval2  15833  smumul  15844  ressinbas  16562  lubdm  17591  glbdm  17604  sylow2a  18746  lsmmod2  18804  lsmdisj2r  18813  ablfac1eu  19197  ressmplbas2  20238  opsrtoslem1  20266  pjdm  20853  rintopn  21519  ordtrest2  21814  cmpsublem  22009  kgentopon  22148  hausdiag  22255  uzrest  22507  ufprim  22519  trust  22840  metnrmlem3  23471  clsocv  23855  ismbl  24129  unmbl  24140  volinun  24149  voliunlem1  24153  ovolioo  24171  itg2cnlem2  24365  ellimc2  24477  limcflf  24481  lhop1lem  24612  lgsquadlem3  25960  rplogsum  26105  umgrislfupgrlem  26909  spthispth  27509  0pth  27906  1pthdlem2  27917  frgrncvvdeqlem3  28082  ex-in  28206  chdmj3i  29262  chdmj4i  29263  chjassi  29265  pjoml2i  29364  pjoml3i  29365  cmcmlem  29370  cmcm2i  29372  cmbr3i  29379  fh3i  29402  fh4i  29403  osumcor2i  29423  mayetes3i  29508  mdslmd3i  30111  mdexchi  30114  atabsi  30180  dmdbr5ati  30201  inin  30279  uniin2  30306  ordtrest2NEW  31168  hasheuni  31346  carsgclctunlem1  31577  eulerpartgbij  31632  fiblem  31658  cvmscld  32522  sate0  32664  msrid  32794  dfpo2  32993  elrn3  33000  noextend  33175  noextendseq  33176  madeval2  33292  bj-inrab3  34249  poimirlem15  34909  mblfinlem2  34932  ftc1anclem6  34974  xrnres2  35653  redundss3  35865  refrelsredund4  35869  pol0N  37047  mapfzcons2  39323  diophrw  39363  conrel2d  40016  iunrelexp0  40054  hashnzfz  40659  disjinfi  41461  fourierdlem80  42478  sge0resplit  42695  sge0split  42698  caragenuncllem  42801