Theorem ineq2i 4158

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

Syntax hints:   = wceq 1542   ∩ cin 3889

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897

This theorem is referenced by:  in4  4175  inindir  4177  indif2  4222  difun1  4240  dfrab3ss  4264  undif1  4417  difdifdir  4432  dfif3  4482  dfif5  4484  disjpr2  4658  disjprsn  4659  disjtp2  4661  intunsn  4930  rint0  4931  riin0  5025  csbres  5942  res0  5943  resres  5952  resundi  5953  resindi  5955  inres  5957  resiun2  5960  resopab  5994  dffr3  6059  dfse2  6060  dminxp  6139  imainrect  6140  cnvrescnv  6154  resdmres  6191  resdifdi  6195  dfpo2  6255  snres0  6257  dfpred2  6270  predidm  6285  funimacnv  6574  fresaun  6706  fresaunres2  6707  tfrlem10  8320  sbthlem5  9023  infssuni  9250  dfsup2  9351  en3lplem2  9528  wemapwe  9612  epfrs  9646  r0weon  9928  infxpenlem  9929  kmlem11  10077  ackbij1lem1  10135  ackbij1lem2  10136  axdc3lem4  10369  canthwelem  10567  dmaddpi  10807  dmmulpi  10808  ssxr  11209  dmhashres  14297  fz1isolem  14417  f1oun2prg  14873  fsumiun  15778  sadeq  16435  bitsres  16436  smuval2  16445  smumul  16456  ressinbas  17209  lubdm  18309  glbdm  18322  sylow2a  19588  lsmmod2  19645  lsmdisj2r  19654  ablfac1eu  20044  pjdm  21700  ressmplbas2  22018  opsrtoslem1  22046  rintopn  22887  ordtrest2  23182  cmpsublem  23377  kgentopon  23516  hausdiag  23623  uzrest  23875  ufprim  23887  trust  24207  metnrmlem3  24840  clsocv  25230  ismbl  25506  unmbl  25517  volinun  25526  voliunlem1  25530  ovolioo  25548  itg2cnlem2  25742  ellimc2  25857  limcflf  25861  lhop1lem  25993  lgsquadlem3  27362  rplogsum  27507  noextend  27647  noextendseq  27648  noetasuplem2  27715  noetainflem2  27719  madeval2  27842  oniso  28280  bdayn0sf1o  28379  umgrislfupgrlem  29208  spthispth  29810  cyclnumvtx  29886  0pth  30213  1pthdlem2  30224  frgrncvvdeqlem3  30389  ex-in  30513  chdmj3i  31572  chdmj4i  31573  chjassi  31575  pjoml2i  31674  pjoml3i  31675  cmcmlem  31680  cmcm2i  31682  cmbr3i  31689  fh3i  31712  fh4i  31713  osumcor2i  31733  mayetes3i  31818  mdslmd3i  32421  mdexchi  32424  atabsi  32490  dmdbr5ati  32511  inin  32604  uniin2  32640  of0r  32770  dfprm3  33631  psrbasfsupp  33690  ordtrest2NEW  34086  hasheuni  34248  carsgclctunlem1  34480  eulerpartgbij  34535  fiblem  34561  cvmscld  35474  sate0  35616  msrid  35746  elrn3  35963  bj-inrab3  37255  poimirlem15  37973  mblfinlem2  37996  ftc1anclem6  38036  dmxrncnvep  38727  dmcnvepres  38728  dmuncnvepres  38729  dmxrnuncnvepres  38730  xrnres2  38764  redundss3  39050  refrelsredund4  39054  dfpetparts2  39310  dfpeters2  39312  pol0N  40372  readvrec2  42810  mapfzcons2  43168  diophrw  43208  conrel2d  44112  iunrelexp0  44150  hashnzfz  44768  wfaxpow  45445  disjinfi  45643  fourierdlem80  46635  sge0resplit  46855  sge0split  46858  caragenuncllem  46961  iscnrm3rlem1  49430