Theorem ineq2i 4170

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

Syntax hints:   = wceq 1570   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3912

This theorem is referenced by:  in4  4186  inindir  4188  indif2  4234  difun1  4252  dfrab3ss  4276  undif1  4437  difdifdir  4452  dfif3  4502  dfif5  4504  disjpr2  4679  disjprsn  4680  disjtp2  4682  intunsn  4952  rint0  4953  uniin2  5040  riin0  5048  csbres  5981  res0  5982  resres  5991  resundi  5992  resindi  5994  inres  5996  resiun2  5999  resopab  6036  dffr3  6101  dfse2  6102  dminxp  6178  imainrect  6179  cnvrescnv  6194  resdmres  6233  resdifdi  6237  dfpo2  6297  snres0  6299  dfpred2  6312  predidm  6327  funimacnv  6617  fresaun  6749  fresaunres2  6750  tfrlem10  8370  sbthlem5  9075  infssuni  9299  dfsup2  9400  en3lplem2  9578  wemapwe  9662  epfrs  9696  r0weon  9992  infxpenlem  9993  kmlem11  10140  ackbij1lem1  10198  ackbij1lem2  10199  axdc3lem4  10432  canthwelem  10630  dmaddpi  10870  dmmulpi  10871  ssxr  11274  dmhashres  14373  fz1isolem  14494  f1oun2prg  14950  fsumiun  15869  sadeq  16525  bitsres  16526  smuval2  16535  smumul  16546  ressinbas  17300  lubdm  18400  glbdm  18413  sylow2a  19684  lsmmod2  19741  lsmdisj2r  19750  ablfac1eu  20140  pjdm  21857  ressmplbas2  22177  opsrtoslem1  22206  rintopn  23066  ordtrest2  23361  cmpsublem  23556  kgentopon  23695  hausdiag  23802  uzrest  24054  ufprim  24066  trust  24386  metnrmlem3  25019  clsocv  25409  ismbl  25685  unmbl  25696  volinun  25705  voliunlem1  25709  ovolioo  25727  itg2cnlem2  25921  ellimc2  26036  limcflf  26040  lhop1lem  26172  lgsquadlem3  27546  rplogsum  27691  noextend  27830  noextendseq  27831  noetasuplem2  27898  noetainflem2  27902  madeval2  28026  oniso  28464  bdayn0sf1o  28563  umgrislfupgrlem  29472  spthispth  30073  cyclnumvtx  30149  0pth  30476  1pthdlem2  30487  frgrncvvdeqlem3  30652  ex-in  30776  chdmj3i  31835  chdmj4i  31836  chjassi  31838  pjoml2i  31937  pjoml3i  31938  cmcmlem  31943  cmcm2i  31945  cmbr3i  31952  fh3i  31975  fh4i  31976  osumcor2i  31996  mayetes3i  32081  mdslmd3i  32684  mdexchi  32687  atabsi  32753  dmdbr5ati  32774  inin  32862  of0r  33024  dfprm3  33843  psrbasfsupp  33901  selvply1rhmlemb  33909  ordtrest2NEW  34313  hasheuni  34475  carsgclctunlem1  34707  eulerpartgbij  34762  fiblem  34788  cvmscld  35765  sate0  35907  msrid  36037  elrn3  36254  bj-inrab3  37585  poimirlem15  38306  mblfinlem2  38329  ftc1anclem6  38369  dmxrncnvep  39058  dmcnvepres  39059  dmuncnvepres  39060  dmxrnuncnvepres  39061  xrnres2  39095  redundss3  39381  refrelsredund4  39385  dfpetparts2  39641  dfpeters2  39643  pol0N  40703  readvrec2  43142  mapfzcons2  43470  diophrw  43510  conrel2d  44410  iunrelexp0  44448  hashnzfz  45050  wfaxpow  45726  disjinfi  45930  fourierdlem80  46920  sge0resplit  47140  sge0split  47143  caragenuncllem  47246  iscnrm3rlem1  49738