Theorem ineq2i 4146

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

Syntax hints:   = wceq 1547   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-in 3890

This theorem is referenced by:  in4  4162  inindir  4164  indif2  4209  difun1  4227  dfrab3ss  4251  undif1  4404  difdifdir  4419  dfif3  4469  dfif5  4471  disjpr2  4645  disjprsn  4646  disjtp2  4648  intunsn  4917  rint0  4918  riin0  5011  csbres  5934  res0  5935  resres  5944  resundi  5945  resindi  5947  inres  5949  resiun2  5952  resopab  5986  dffr3  6051  dfse2  6052  dminxp  6131  imainrect  6132  cnvrescnv  6146  resdmres  6183  resdifdi  6187  dfpo2  6247  snres0  6249  dfpred2  6262  predidm  6277  funimacnv  6566  fresaun  6698  fresaunres2  6699  tfrlem10  8316  sbthlem5  9019  infssuni  9246  dfsup2  9347  en3lplem2  9525  wemapwe  9609  epfrs  9643  r0weon  9925  infxpenlem  9926  kmlem11  10074  ackbij1lem1  10132  ackbij1lem2  10133  axdc3lem4  10366  canthwelem  10564  dmaddpi  10804  dmmulpi  10805  ssxr  11206  dmhashres  14294  fz1isolem  14414  f1oun2prg  14870  fsumiun  15775  sadeq  16432  bitsres  16433  smuval2  16442  smumul  16453  ressinbas  17206  lubdm  18306  glbdm  18319  sylow2a  19585  lsmmod2  19642  lsmdisj2r  19651  ablfac1eu  20041  pjdm  21682  ressmplbas2  22002  opsrtoslem1  22031  rintopn  22892  ordtrest2  23187  cmpsublem  23382  kgentopon  23521  hausdiag  23628  uzrest  23880  ufprim  23892  trust  24212  metnrmlem3  24845  clsocv  25235  ismbl  25511  unmbl  25522  volinun  25531  voliunlem1  25535  ovolioo  25553  itg2cnlem2  25747  ellimc2  25862  limcflf  25866  lhop1lem  25998  lgsquadlem3  27363  rplogsum  27508  noextend  27648  noextendseq  27649  noetasuplem2  27716  noetainflem2  27720  madeval2  27843  oniso  28281  bdayn0sf1o  28380  umgrislfupgrlem  29209  spthispth  29810  cyclnumvtx  29886  0pth  30213  1pthdlem2  30224  frgrncvvdeqlem3  30389  ex-in  30513  chdmj3i  31572  chdmj4i  31573  chjassi  31575  pjoml2i  31674  pjoml3i  31675  cmcmlem  31680  cmcm2i  31682  cmbr3i  31689  fh3i  31712  fh4i  31713  osumcor2i  31733  mayetes3i  31818  mdslmd3i  32421  mdexchi  32424  atabsi  32490  dmdbr5ati  32511  inin  32604  uniin2  32641  of0r  32771  dfprm3  33636  psrbasfsupp  33695  selvply1rhmlemb  33703  ordtrest2NEW  34107  hasheuni  34269  carsgclctunlem1  34501  eulerpartgbij  34556  fiblem  34582  cvmscld  35501  sate0  35643  msrid  35773  elrn3  35990  bj-inrab3  37282  poimirlem15  38002  mblfinlem2  38025  ftc1anclem6  38065  dmxrncnvep  38756  dmcnvepres  38757  dmuncnvepres  38758  dmxrnuncnvepres  38759  xrnres2  38793  redundss3  39079  refrelsredund4  39083  dfpetparts2  39339  dfpeters2  39341  pol0N  40401  readvrec2  42838  mapfzcons2  43168  diophrw  43208  conrel2d  44108  iunrelexp0  44146  hashnzfz  44764  wfaxpow  45441  disjinfi  45639  fourierdlem80  46629  sge0resplit  46849  sge0split  46852  caragenuncllem  46955  iscnrm3rlem1  49430