Theorem ineq2i 4169

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

Syntax hints:   = wceq 1541   ∩ cin 3909

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-in 3917

This theorem is referenced by:  in4  4185  inindir  4187  indif2  4230  difun1  4249  dfrab3ss  4272  undif1  4435  difdifdir  4449  dfif3  4500  dfif5  4502  disjpr2  4674  disjprsn  4675  disjtp2  4677  intunsn  4950  rint0  4951  riin0  5042  csbres  5940  res0  5941  resres  5950  resundi  5951  resindi  5953  inres  5955  resiun2  5958  resopab  5988  dffr3  6051  dfse2  6052  dminxp  6132  imainrect  6133  cnvrescnv  6147  resdmres  6184  resdifdi  6188  dfpo2  6248  snres0  6250  dfpred2  6263  predidm  6280  funimacnv  6582  fresaun  6713  fresaunres2  6714  wfrlem13OLD  8266  tfrlem10  8332  sbthlem5  9030  infssuni  9286  dfsup2  9379  en3lplem2  9548  wemapwe  9632  epfrs  9666  r0weon  9947  infxpenlem  9948  kmlem11  10095  ackbij1lem1  10155  ackbij1lem2  10156  axdc3lem4  10388  canthwelem  10585  dmaddpi  10825  dmmulpi  10826  ssxr  11223  dmhashres  14240  fz1isolem  14359  f1oun2prg  14805  fsumiun  15705  sadeq  16351  bitsres  16352  smuval2  16361  smumul  16372  ressinbas  17125  lubdm  18239  glbdm  18252  sylow2a  19399  lsmmod2  19456  lsmdisj2r  19465  ablfac1eu  19850  pjdm  21111  ressmplbas2  21426  opsrtoslem1  21460  rintopn  22256  ordtrest2  22553  cmpsublem  22748  kgentopon  22887  hausdiag  22994  uzrest  23246  ufprim  23258  trust  23579  metnrmlem3  24222  clsocv  24612  ismbl  24888  unmbl  24899  volinun  24908  voliunlem1  24912  ovolioo  24930  itg2cnlem2  25125  ellimc2  25239  limcflf  25243  lhop1lem  25375  lgsquadlem3  26728  rplogsum  26873  noextend  27012  noextendseq  27013  noetasuplem2  27080  noetainflem2  27084  madeval2  27181  umgrislfupgrlem  28020  spthispth  28621  0pth  29016  1pthdlem2  29027  frgrncvvdeqlem3  29192  ex-in  29316  chdmj3i  30372  chdmj4i  30373  chjassi  30375  pjoml2i  30474  pjoml3i  30475  cmcmlem  30480  cmcm2i  30482  cmbr3i  30489  fh3i  30512  fh4i  30513  osumcor2i  30533  mayetes3i  30618  mdslmd3i  31221  mdexchi  31224  atabsi  31290  dmdbr5ati  31311  inin  31389  uniin2  31418  ordtrest2NEW  32444  hasheuni  32624  carsgclctunlem1  32857  eulerpartgbij  32912  fiblem  32938  cvmscld  33807  sate0  33949  msrid  34079  elrn3  34275  bj-inrab3  35389  poimirlem15  36083  mblfinlem2  36106  ftc1anclem6  36146  xrnres2  36855  redundss3  37080  refrelsredund4  37084  pol0N  38362  mapfzcons2  41019  diophrw  41059  conrel2d  41917  iunrelexp0  41955  hashnzfz  42581  disjinfi  43387  fourierdlem80  44398  sge0resplit  44618  sge0split  44621  caragenuncllem  44724  iscnrm3rlem1  46944