Theorem ineq2i 4238

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

Syntax hints:   = wceq 1537   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983

This theorem is referenced by:  in4  4255  inindir  4257  indif2  4300  difun1  4318  dfrab3ss  4342  undif1  4499  difdifdir  4515  dfif3  4562  dfif5  4564  disjpr2  4738  disjprsn  4739  disjtp2  4741  intunsn  5011  rint0  5012  riin0  5105  csbres  6012  res0  6013  resres  6022  resundi  6023  resindi  6025  inres  6027  resiun2  6030  resopab  6063  dffr3  6129  dfse2  6130  dminxp  6211  imainrect  6212  cnvrescnv  6226  resdmres  6263  resdifdi  6267  dfpo2  6327  snres0  6329  dfpred2  6342  predidm  6358  funimacnv  6659  fresaun  6792  fresaunres2  6793  wfrlem13OLD  8377  tfrlem10  8443  sbthlem5  9153  infssuni  9414  dfsup2  9513  en3lplem2  9682  wemapwe  9766  epfrs  9800  r0weon  10081  infxpenlem  10082  kmlem11  10230  ackbij1lem1  10288  ackbij1lem2  10289  axdc3lem4  10522  canthwelem  10719  dmaddpi  10959  dmmulpi  10960  ssxr  11359  dmhashres  14390  fz1isolem  14510  f1oun2prg  14966  fsumiun  15869  sadeq  16518  bitsres  16519  smuval2  16528  smumul  16539  ressinbas  17304  lubdm  18421  glbdm  18434  sylow2a  19661  lsmmod2  19718  lsmdisj2r  19727  ablfac1eu  20117  pjdm  21750  ressmplbas2  22068  opsrtoslem1  22102  rintopn  22936  ordtrest2  23233  cmpsublem  23428  kgentopon  23567  hausdiag  23674  uzrest  23926  ufprim  23938  trust  24259  metnrmlem3  24902  clsocv  25303  ismbl  25580  unmbl  25591  volinun  25600  voliunlem1  25604  ovolioo  25622  itg2cnlem2  25817  ellimc2  25932  limcflf  25936  lhop1lem  26072  lgsquadlem3  27444  rplogsum  27589  noextend  27729  noextendseq  27730  noetasuplem2  27797  noetainflem2  27801  madeval2  27910  umgrislfupgrlem  29157  spthispth  29762  0pth  30157  1pthdlem2  30168  frgrncvvdeqlem3  30333  ex-in  30457  chdmj3i  31515  chdmj4i  31516  chjassi  31518  pjoml2i  31617  pjoml3i  31618  cmcmlem  31623  cmcm2i  31625  cmbr3i  31632  fh3i  31655  fh4i  31656  osumcor2i  31676  mayetes3i  31761  mdslmd3i  32364  mdexchi  32367  atabsi  32433  dmdbr5ati  32454  inin  32545  uniin2  32575  of0r  32696  dfprm3  33546  ordtrest2NEW  33869  hasheuni  34049  carsgclctunlem1  34282  eulerpartgbij  34337  fiblem  34363  cvmscld  35241  sate0  35383  msrid  35513  elrn3  35724  bj-inrab3  36895  poimirlem15  37595  mblfinlem2  37618  ftc1anclem6  37658  xrnres2  38359  redundss3  38584  refrelsredund4  38588  pol0N  39866  mapfzcons2  42675  diophrw  42715  conrel2d  43626  iunrelexp0  43664  hashnzfz  44289  disjinfi  45099  fourierdlem80  46107  sge0resplit  46327  sge0split  46330  caragenuncllem  46433  iscnrm3rlem1  48620