Theorem ineq2i 4180

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

Syntax hints:   = wceq 1540   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921

This theorem is referenced by:  in4  4197  inindir  4199  indif2  4244  difun1  4262  dfrab3ss  4286  undif1  4439  difdifdir  4455  dfif3  4503  dfif5  4505  disjpr2  4677  disjprsn  4678  disjtp2  4680  intunsn  4951  rint0  4952  riin0  5046  csbres  5953  res0  5954  resres  5963  resundi  5964  resindi  5966  inres  5968  resiun2  5971  resopab  6005  dffr3  6070  dfse2  6071  dminxp  6153  imainrect  6154  cnvrescnv  6168  resdmres  6205  resdifdi  6209  dfpo2  6269  snres0  6271  dfpred2  6284  predidm  6299  funimacnv  6597  fresaun  6731  fresaunres2  6732  tfrlem10  8355  sbthlem5  9055  infssuni  9297  dfsup2  9395  en3lplem2  9566  wemapwe  9650  epfrs  9684  r0weon  9965  infxpenlem  9966  kmlem11  10114  ackbij1lem1  10172  ackbij1lem2  10173  axdc3lem4  10406  canthwelem  10603  dmaddpi  10843  dmmulpi  10844  ssxr  11243  dmhashres  14306  fz1isolem  14426  f1oun2prg  14883  fsumiun  15787  sadeq  16442  bitsres  16443  smuval2  16452  smumul  16463  ressinbas  17215  lubdm  18310  glbdm  18323  sylow2a  19549  lsmmod2  19606  lsmdisj2r  19615  ablfac1eu  20005  pjdm  21616  ressmplbas2  21934  opsrtoslem1  21962  rintopn  22796  ordtrest2  23091  cmpsublem  23286  kgentopon  23425  hausdiag  23532  uzrest  23784  ufprim  23796  trust  24117  metnrmlem3  24750  clsocv  25150  ismbl  25427  unmbl  25438  volinun  25447  voliunlem1  25451  ovolioo  25469  itg2cnlem2  25663  ellimc2  25778  limcflf  25782  lhop1lem  25918  lgsquadlem3  27293  rplogsum  27438  noextend  27578  noextendseq  27579  noetasuplem2  27646  noetainflem2  27650  madeval2  27761  onsiso  28169  bdayn0sf1o  28259  umgrislfupgrlem  29049  spthispth  29654  cyclnumvtx  29730  0pth  30054  1pthdlem2  30065  frgrncvvdeqlem3  30230  ex-in  30354  chdmj3i  31412  chdmj4i  31413  chjassi  31415  pjoml2i  31514  pjoml3i  31515  cmcmlem  31520  cmcm2i  31522  cmbr3i  31529  fh3i  31552  fh4i  31553  osumcor2i  31573  mayetes3i  31658  mdslmd3i  32261  mdexchi  32264  atabsi  32330  dmdbr5ati  32351  inin  32445  uniin2  32481  of0r  32602  dfprm3  33524  ordtrest2NEW  33913  hasheuni  34075  carsgclctunlem1  34308  eulerpartgbij  34363  fiblem  34389  cvmscld  35260  sate0  35402  msrid  35532  elrn3  35749  bj-inrab3  36917  poimirlem15  37629  mblfinlem2  37652  ftc1anclem6  37692  dmxrncnvep  38362  xrnres2  38389  redundss3  38619  refrelsredund4  38623  pol0N  39903  readvrec2  42349  mapfzcons2  42707  diophrw  42747  conrel2d  43653  iunrelexp0  43691  hashnzfz  44309  wfaxpow  44987  disjinfi  45186  fourierdlem80  46184  sge0resplit  46404  sge0split  46407  caragenuncllem  46510  iscnrm3rlem1  48925