Theorem ineq2i 4163

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

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  in4  4179  inindir  4181  indif2  4227  difun1  4245  dfrab3ss  4269  undif1  4430  difdifdir  4447  dfif3  4497  dfif5  4499  disjpr2  4674  disjprsn  4675  disjtp2  4677  intunsn  4947  rint0  4948  uniin2  5034  riin0  5042  csbres  5975  res0  5976  resres  5985  resundi  5986  resindi  5988  inres  5990  resiun2  5993  resopab  6030  dffr3  6095  dfse2  6096  dminxp  6173  imainrect  6174  cnvrescnv  6189  resdmres  6228  resdifdi  6232  dfpo2  6294  snres0  6296  dfpred2  6309  predidm  6324  funimacnv  6614  fresaun  6746  fresaunres2  6747  tfrlem10  8376  sbthlem5  9089  infssuni  9313  dfsup2  9414  en3lplem2  9592  wemapwe  9676  epfrs  9710  r0weon  10015  infxpenlem  10016  kmlem11  10163  ackbij1lem1  10221  ackbij1lem2  10222  axdc3lem4  10455  canthwelem  10659  dmaddpi  10899  dmmulpi  10900  ssxr  11303  dmhashres  14405  fz1isolem  14526  f1oun2prg  14988  fsumiun  15908  sadeq  16562  bitsres  16563  smuval2  16572  smumul  16583  ressinbas  17337  lubdm  18437  glbdm  18450  sylow2a  19746  lsmmod2  19803  lsmdisj2r  19812  ablfac1eu  20202  pjdm  21920  ressmplbas2  22242  opsrtoslem1  22271  rintopn  23134  ordtrest2  23429  cmpsublem  23624  kgentopon  23764  hausdiag  23871  uzrest  24123  ufprim  24135  trust  24455  metnrmlem3  25088  clsocv  25478  ismbl  25754  unmbl  25765  volinun  25774  voliunlem1  25778  ovolioo  25796  itg2cnlem2  25990  ellimc2  26104  limcflf  26108  lhop1lem  26240  lgsquadlem3  27618  rplogsum  27763  noextend  27902  noextendseq  27903  noetasuplem2  27970  noetainflem2  27974  madeval2  28098  oniso  28536  bdayn0sf1o  28635  umgrislfupgrlem  29579  spthispth  30188  cyclnumvtx  30267  0pth  30595  1pthdlem2  30606  frgrncvvdeqlem3  30781  ex-in  30905  chdmj3i  31964  chdmj4i  31965  chjassi  31967  pjoml2i  32066  pjoml3i  32067  cmcmlem  32072  cmcm2i  32074  cmbr3i  32081  fh3i  32104  fh4i  32105  osumcor2i  32125  mayetes3i  32210  mdslmd3i  32813  mdexchi  32816  atabsi  32882  dmdbr5ati  32903  inin  32991  of0r  33152  dfprm3  33963  psrbasfsupp  34021  selvply1rhmlemb  34029  ordtrest2NEW  34433  hasheuni  34595  carsgclctunlem1  34828  eulerpartgbij  34883  fiblem  34909  cvmscld  35852  sate0  35994  msrid  36124  elrn3  36341  bj-inrab3  37673  poimirlem15  38384  mblfinlem2  38407  ftc1anclem6  38447  dmxrncnvep  39137  dmcnvepres  39138  dmuncnvepres  39139  dmxrnuncnvepres  39140  xrnres2  39174  redundss3  39460  refrelsredund4  39464  dfpetparts2  39720  dfpeters2  39722  pol0N  40782  readvrec2  43236  mapfzcons2  43564  diophrw  43604  conrel2d  44504  iunrelexp0  44542  hashnzfz  45144  wfaxpow  45820  disjinfi  46024  fourierdlem80  47014  sge0resplit  47234  sge0split  47237  caragenuncllem  47340  iscnrm3rlem1  49866