Theorem ineq2i 4157

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

Syntax hints:   = wceq 1542   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896

This theorem is referenced by:  in4  4174  inindir  4176  indif2  4221  difun1  4239  dfrab3ss  4263  undif1  4416  difdifdir  4431  dfif3  4481  dfif5  4483  disjpr2  4657  disjprsn  4658  disjtp2  4660  intunsn  4929  rint0  4930  riin0  5024  csbres  5947  res0  5948  resres  5957  resundi  5958  resindi  5960  inres  5962  resiun2  5965  resopab  5999  dffr3  6064  dfse2  6065  dminxp  6144  imainrect  6145  cnvrescnv  6159  resdmres  6196  resdifdi  6200  dfpo2  6260  snres0  6262  dfpred2  6275  predidm  6290  funimacnv  6579  fresaun  6711  fresaunres2  6712  tfrlem10  8326  sbthlem5  9029  infssuni  9256  dfsup2  9357  en3lplem2  9534  wemapwe  9618  epfrs  9652  r0weon  9934  infxpenlem  9935  kmlem11  10083  ackbij1lem1  10141  ackbij1lem2  10142  axdc3lem4  10375  canthwelem  10573  dmaddpi  10813  dmmulpi  10814  ssxr  11215  dmhashres  14303  fz1isolem  14423  f1oun2prg  14879  fsumiun  15784  sadeq  16441  bitsres  16442  smuval2  16451  smumul  16462  ressinbas  17215  lubdm  18315  glbdm  18328  sylow2a  19594  lsmmod2  19651  lsmdisj2r  19660  ablfac1eu  20050  pjdm  21687  ressmplbas2  22005  opsrtoslem1  22033  rintopn  22874  ordtrest2  23169  cmpsublem  23364  kgentopon  23503  hausdiag  23610  uzrest  23862  ufprim  23874  trust  24194  metnrmlem3  24827  clsocv  25217  ismbl  25493  unmbl  25504  volinun  25513  voliunlem1  25517  ovolioo  25535  itg2cnlem2  25729  ellimc2  25844  limcflf  25848  lhop1lem  25980  lgsquadlem3  27345  rplogsum  27490  noextend  27630  noextendseq  27631  noetasuplem2  27698  noetainflem2  27702  madeval2  27825  oniso  28263  bdayn0sf1o  28362  umgrislfupgrlem  29191  spthispth  29792  cyclnumvtx  29868  0pth  30195  1pthdlem2  30206  frgrncvvdeqlem3  30371  ex-in  30495  chdmj3i  31554  chdmj4i  31555  chjassi  31557  pjoml2i  31656  pjoml3i  31657  cmcmlem  31662  cmcm2i  31664  cmbr3i  31671  fh3i  31694  fh4i  31695  osumcor2i  31715  mayetes3i  31800  mdslmd3i  32403  mdexchi  32406  atabsi  32472  dmdbr5ati  32493  inin  32586  uniin2  32622  of0r  32752  dfprm3  33613  psrbasfsupp  33672  ordtrest2NEW  34067  hasheuni  34229  carsgclctunlem1  34461  eulerpartgbij  34516  fiblem  34542  cvmscld  35455  sate0  35597  msrid  35727  elrn3  35944  bj-inrab3  37236  poimirlem15  37956  mblfinlem2  37979  ftc1anclem6  38019  dmxrncnvep  38710  dmcnvepres  38711  dmuncnvepres  38712  dmxrnuncnvepres  38713  xrnres2  38747  redundss3  39033  refrelsredund4  39037  dfpetparts2  39293  dfpeters2  39295  pol0N  40355  readvrec2  42793  mapfzcons2  43151  diophrw  43191  conrel2d  44091  iunrelexp0  44129  hashnzfz  44747  wfaxpow  45424  disjinfi  45622  fourierdlem80  46614  sge0resplit  46834  sge0split  46837  caragenuncllem  46940  iscnrm3rlem1  49415