Theorem ineq2i 4164

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

Syntax hints:   = wceq 1541   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3904

This theorem is referenced by:  in4  4181  inindir  4183  indif2  4228  difun1  4246  dfrab3ss  4270  undif1  4423  difdifdir  4439  dfif3  4487  dfif5  4489  disjpr2  4663  disjprsn  4664  disjtp2  4666  intunsn  4935  rint0  4936  riin0  5028  csbres  5930  res0  5931  resres  5940  resundi  5941  resindi  5943  inres  5945  resiun2  5948  resopab  5982  dffr3  6047  dfse2  6048  dminxp  6127  imainrect  6128  cnvrescnv  6142  resdmres  6179  resdifdi  6183  dfpo2  6243  snres0  6245  dfpred2  6258  predidm  6273  funimacnv  6562  fresaun  6694  fresaunres2  6695  tfrlem10  8306  sbthlem5  9004  infssuni  9230  dfsup2  9328  en3lplem2  9503  wemapwe  9587  epfrs  9621  r0weon  9903  infxpenlem  9904  kmlem11  10052  ackbij1lem1  10110  ackbij1lem2  10111  axdc3lem4  10344  canthwelem  10541  dmaddpi  10781  dmmulpi  10782  ssxr  11182  dmhashres  14248  fz1isolem  14368  f1oun2prg  14824  fsumiun  15728  sadeq  16383  bitsres  16384  smuval2  16393  smumul  16404  ressinbas  17156  lubdm  18255  glbdm  18268  sylow2a  19531  lsmmod2  19588  lsmdisj2r  19597  ablfac1eu  19987  pjdm  21644  ressmplbas2  21962  opsrtoslem1  21990  rintopn  22824  ordtrest2  23119  cmpsublem  23314  kgentopon  23453  hausdiag  23560  uzrest  23812  ufprim  23824  trust  24144  metnrmlem3  24777  clsocv  25177  ismbl  25454  unmbl  25465  volinun  25474  voliunlem1  25478  ovolioo  25496  itg2cnlem2  25690  ellimc2  25805  limcflf  25809  lhop1lem  25945  lgsquadlem3  27320  rplogsum  27465  noextend  27605  noextendseq  27606  noetasuplem2  27673  noetainflem2  27677  madeval2  27794  onsiso  28205  bdayn0sf1o  28295  umgrislfupgrlem  29100  spthispth  29702  cyclnumvtx  29778  0pth  30105  1pthdlem2  30116  frgrncvvdeqlem3  30281  ex-in  30405  chdmj3i  31463  chdmj4i  31464  chjassi  31466  pjoml2i  31565  pjoml3i  31566  cmcmlem  31571  cmcm2i  31573  cmbr3i  31580  fh3i  31603  fh4i  31604  osumcor2i  31624  mayetes3i  31709  mdslmd3i  32312  mdexchi  32315  atabsi  32381  dmdbr5ati  32402  inin  32496  uniin2  32532  of0r  32660  dfprm3  33518  psrbasfsupp  33572  ordtrest2NEW  33936  hasheuni  34098  carsgclctunlem1  34330  eulerpartgbij  34385  fiblem  34411  cvmscld  35317  sate0  35459  msrid  35589  elrn3  35806  bj-inrab3  36973  poimirlem15  37685  mblfinlem2  37708  ftc1anclem6  37748  dmxrncnvep  38423  dmcnvepres  38424  dmuncnvepres  38425  dmxrnuncnvepres  38426  xrnres2  38460  redundss3  38734  refrelsredund4  38738  pol0N  40018  readvrec2  42464  mapfzcons2  42822  diophrw  42862  conrel2d  43767  iunrelexp0  43805  hashnzfz  44423  wfaxpow  45100  disjinfi  45299  fourierdlem80  46294  sge0resplit  46514  sge0split  46517  caragenuncllem  46620  iscnrm3rlem1  49050