Theorem ineq2i 4178

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

Syntax hints:   = wceq 1567   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920

This theorem is referenced by:  in4  4194  inindir  4196  indif2  4242  difun1  4260  dfrab3ss  4284  undif1  4442  difdifdir  4457  dfif3  4507  dfif5  4509  disjpr2  4684  disjprsn  4685  disjtp2  4687  intunsn  4956  rint0  4957  uniin2  5044  riin0  5052  csbres  5982  res0  5983  resres  5992  resundi  5993  resindi  5995  inres  5997  resiun2  6000  resopab  6037  dffr3  6102  dfse2  6103  dminxp  6179  imainrect  6180  cnvrescnv  6195  resdmres  6234  resdifdi  6238  dfpo2  6298  snres0  6300  dfpred2  6313  predidm  6328  funimacnv  6618  fresaun  6750  fresaunres2  6751  tfrlem10  8374  sbthlem5  9079  infssuni  9303  dfsup2  9404  en3lplem2  9582  wemapwe  9666  epfrs  9700  r0weon  9996  infxpenlem  9997  kmlem11  10144  ackbij1lem1  10202  ackbij1lem2  10203  axdc3lem4  10437  canthwelem  10635  dmaddpi  10875  dmmulpi  10876  ssxr  11279  dmhashres  14377  fz1isolem  14498  f1oun2prg  14954  fsumiun  15873  sadeq  16530  bitsres  16531  smuval2  16540  smumul  16551  ressinbas  17305  lubdm  18405  glbdm  18418  sylow2a  19689  lsmmod2  19746  lsmdisj2r  19755  ablfac1eu  20145  pjdm  21826  ressmplbas2  22146  opsrtoslem1  22175  rintopn  23035  ordtrest2  23330  cmpsublem  23525  kgentopon  23664  hausdiag  23771  uzrest  24023  ufprim  24035  trust  24355  metnrmlem3  24988  clsocv  25378  ismbl  25654  unmbl  25665  volinun  25674  voliunlem1  25678  ovolioo  25696  itg2cnlem2  25890  ellimc2  26005  limcflf  26009  lhop1lem  26141  lgsquadlem3  27512  rplogsum  27657  noextend  27796  noextendseq  27797  noetasuplem2  27864  noetainflem2  27868  madeval2  27992  oniso  28430  bdayn0sf1o  28529  umgrislfupgrlem  29413  spthispth  30014  cyclnumvtx  30090  0pth  30417  1pthdlem2  30428  frgrncvvdeqlem3  30593  ex-in  30717  chdmj3i  31776  chdmj4i  31777  chjassi  31779  pjoml2i  31878  pjoml3i  31879  cmcmlem  31884  cmcm2i  31886  cmbr3i  31893  fh3i  31916  fh4i  31917  osumcor2i  31937  mayetes3i  32022  mdslmd3i  32625  mdexchi  32628  atabsi  32694  dmdbr5ati  32715  inin  32803  of0r  32965  dfprm3  33788  psrbasfsupp  33846  selvply1rhmlemb  33854  ordtrest2NEW  34258  hasheuni  34420  carsgclctunlem1  34652  eulerpartgbij  34707  fiblem  34733  cvmscld  35664  sate0  35806  msrid  35936  elrn3  36153  bj-inrab3  37453  poimirlem15  38174  mblfinlem2  38197  ftc1anclem6  38237  dmxrncnvep  38928  dmcnvepres  38929  dmuncnvepres  38930  dmxrnuncnvepres  38931  xrnres2  38965  redundss3  39251  refrelsredund4  39255  dfpetparts2  39511  dfpeters2  39513  pol0N  40573  readvrec2  43012  mapfzcons2  43342  diophrw  43382  conrel2d  44282  iunrelexp0  44320  hashnzfz  44922  wfaxpow  45598  disjinfi  45802  fourierdlem80  46792  sge0resplit  47012  sge0split  47015  caragenuncllem  47118  iscnrm3rlem1  49603