Theorem ineq2i 4168

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

Syntax hints:   = wceq 1540   ∩ cin 3902

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 3395  df-in 3910

This theorem is referenced by:  in4  4185  inindir  4187  indif2  4232  difun1  4250  dfrab3ss  4274  undif1  4427  difdifdir  4443  dfif3  4491  dfif5  4493  disjpr2  4665  disjprsn  4666  disjtp2  4668  intunsn  4937  rint0  4938  riin0  5031  csbres  5933  res0  5934  resres  5943  resundi  5944  resindi  5946  inres  5948  resiun2  5951  resopab  5985  dffr3  6050  dfse2  6051  dminxp  6129  imainrect  6130  cnvrescnv  6144  resdmres  6181  resdifdi  6185  dfpo2  6244  snres0  6246  dfpred2  6259  predidm  6274  funimacnv  6563  fresaun  6695  fresaunres2  6696  tfrlem10  8309  sbthlem5  9008  infssuni  9236  dfsup2  9334  en3lplem2  9509  wemapwe  9593  epfrs  9627  r0weon  9906  infxpenlem  9907  kmlem11  10055  ackbij1lem1  10113  ackbij1lem2  10114  axdc3lem4  10347  canthwelem  10544  dmaddpi  10784  dmmulpi  10785  ssxr  11185  dmhashres  14248  fz1isolem  14368  f1oun2prg  14824  fsumiun  15728  sadeq  16383  bitsres  16384  smuval2  16393  smumul  16404  ressinbas  17156  lubdm  18255  glbdm  18268  sylow2a  19498  lsmmod2  19555  lsmdisj2r  19564  ablfac1eu  19954  pjdm  21614  ressmplbas2  21932  opsrtoslem1  21960  rintopn  22794  ordtrest2  23089  cmpsublem  23284  kgentopon  23423  hausdiag  23530  uzrest  23782  ufprim  23794  trust  24115  metnrmlem3  24748  clsocv  25148  ismbl  25425  unmbl  25436  volinun  25445  voliunlem1  25449  ovolioo  25467  itg2cnlem2  25661  ellimc2  25776  limcflf  25780  lhop1lem  25916  lgsquadlem3  27291  rplogsum  27436  noextend  27576  noextendseq  27577  noetasuplem2  27644  noetainflem2  27648  madeval2  27763  onsiso  28174  bdayn0sf1o  28264  umgrislfupgrlem  29067  spthispth  29669  cyclnumvtx  29745  0pth  30069  1pthdlem2  30080  frgrncvvdeqlem3  30245  ex-in  30369  chdmj3i  31427  chdmj4i  31428  chjassi  31430  pjoml2i  31529  pjoml3i  31530  cmcmlem  31535  cmcm2i  31537  cmbr3i  31544  fh3i  31567  fh4i  31568  osumcor2i  31588  mayetes3i  31673  mdslmd3i  32276  mdexchi  32279  atabsi  32345  dmdbr5ati  32366  inin  32460  uniin2  32496  of0r  32621  dfprm3  33490  psrbasfsupp  33544  ordtrest2NEW  33890  hasheuni  34052  carsgclctunlem1  34285  eulerpartgbij  34340  fiblem  34366  cvmscld  35250  sate0  35392  msrid  35522  elrn3  35739  bj-inrab3  36907  poimirlem15  37619  mblfinlem2  37642  ftc1anclem6  37682  dmxrncnvep  38352  xrnres2  38379  redundss3  38609  refrelsredund4  38613  pol0N  39892  readvrec2  42338  mapfzcons2  42696  diophrw  42736  conrel2d  43641  iunrelexp0  43679  hashnzfz  44297  wfaxpow  44975  disjinfi  45174  fourierdlem80  46171  sge0resplit  46391  sge0split  46394  caragenuncllem  46497  iscnrm3rlem1  48928