Theorem ineq2i 4185

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

Syntax hints:   = wceq 1533   ∩ cin 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3942

This theorem is referenced by:  in4  4201  inindir  4203  indif2  4246  difun1  4263  dfrab3ss  4280  undif1  4423  difdifdir  4436  dfif3  4480  dfif5  4482  disjpr2  4648  disjprsn  4649  disjtp2  4651  intunsn  4914  rint0  4915  riin0  5003  csbres  5855  res0  5856  resres  5865  resundi  5866  resindi  5868  inres  5870  resiun2  5873  resopab  5901  dffr3  5961  dfse2  5962  dminxp  6036  imainrect  6037  cnvrescnv  6051  resdmres  6088  dfpred2  6156  predidm  6169  funimacnv  6434  fresaun  6548  fresaunres2  6549  wfrlem13  7966  tfrlem10  8022  sbthlem5  8630  infssuni  8814  dfsup2  8907  en3lplem2  9075  wemapwe  9159  epfrs  9172  r0weon  9437  infxpenlem  9438  kmlem11  9585  ackbij1lem1  9641  ackbij1lem2  9642  axdc3lem4  9874  canthwelem  10071  dmaddpi  10311  dmmulpi  10312  ssxr  10709  dmhashres  13700  fz1isolem  13818  f1oun2prg  14278  fsumiun  15175  sadeq  15820  bitsres  15821  smuval2  15830  smumul  15841  ressinbas  16559  lubdm  17588  glbdm  17601  sylow2a  18743  lsmmod2  18801  lsmdisj2r  18810  ablfac1eu  19194  ressmplbas2  20235  opsrtoslem1  20263  pjdm  20850  rintopn  21516  ordtrest2  21811  cmpsublem  22006  kgentopon  22145  hausdiag  22252  uzrest  22504  ufprim  22516  trust  22837  metnrmlem3  23468  clsocv  23852  ismbl  24126  unmbl  24137  volinun  24146  voliunlem1  24150  ovolioo  24168  itg2cnlem2  24362  ellimc2  24474  limcflf  24478  lhop1lem  24609  lgsquadlem3  25957  rplogsum  26102  umgrislfupgrlem  26906  spthispth  27506  0pth  27903  1pthdlem2  27914  frgrncvvdeqlem3  28079  ex-in  28203  chdmj3i  29259  chdmj4i  29260  chjassi  29262  pjoml2i  29361  pjoml3i  29362  cmcmlem  29367  cmcm2i  29369  cmbr3i  29376  fh3i  29399  fh4i  29400  osumcor2i  29420  mayetes3i  29505  mdslmd3i  30108  mdexchi  30111  atabsi  30177  dmdbr5ati  30198  inin  30276  uniin2  30303  ordtrest2NEW  31166  hasheuni  31344  carsgclctunlem1  31575  eulerpartgbij  31630  fiblem  31656  cvmscld  32520  sate0  32662  msrid  32792  dfpo2  32991  elrn3  32998  noextend  33173  noextendseq  33174  madeval2  33290  bj-inrab3  34247  poimirlem15  34906  mblfinlem2  34929  ftc1anclem6  34971  xrnres2  35650  redundss3  35862  refrelsredund4  35866  pol0N  37044  mapfzcons2  39314  diophrw  39354  conrel2d  40007  iunrelexp0  40045  hashnzfz  40650  disjinfi  41452  fourierdlem80  42470  sge0resplit  42687  sge0split  42690  caragenuncllem  42793