Theorem ineq2i 4217

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

Syntax hints:   = wceq 1540   ∩ cin 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958

This theorem is referenced by:  in4  4234  inindir  4236  indif2  4281  difun1  4299  dfrab3ss  4323  undif1  4476  difdifdir  4492  dfif3  4540  dfif5  4542  disjpr2  4713  disjprsn  4714  disjtp2  4716  intunsn  4987  rint0  4988  riin0  5082  csbres  6000  res0  6001  resres  6010  resundi  6011  resindi  6013  inres  6015  resiun2  6018  resopab  6052  dffr3  6117  dfse2  6118  dminxp  6200  imainrect  6201  cnvrescnv  6215  resdmres  6252  resdifdi  6256  dfpo2  6316  snres0  6318  dfpred2  6331  predidm  6347  funimacnv  6647  fresaun  6779  fresaunres2  6780  wfrlem13OLD  8361  tfrlem10  8427  sbthlem5  9127  infssuni  9386  dfsup2  9484  en3lplem2  9653  wemapwe  9737  epfrs  9771  r0weon  10052  infxpenlem  10053  kmlem11  10201  ackbij1lem1  10259  ackbij1lem2  10260  axdc3lem4  10493  canthwelem  10690  dmaddpi  10930  dmmulpi  10931  ssxr  11330  dmhashres  14380  fz1isolem  14500  f1oun2prg  14956  fsumiun  15857  sadeq  16509  bitsres  16510  smuval2  16519  smumul  16530  ressinbas  17291  lubdm  18396  glbdm  18409  sylow2a  19637  lsmmod2  19694  lsmdisj2r  19703  ablfac1eu  20093  pjdm  21727  ressmplbas2  22045  opsrtoslem1  22079  rintopn  22915  ordtrest2  23212  cmpsublem  23407  kgentopon  23546  hausdiag  23653  uzrest  23905  ufprim  23917  trust  24238  metnrmlem3  24883  clsocv  25284  ismbl  25561  unmbl  25572  volinun  25581  voliunlem1  25585  ovolioo  25603  itg2cnlem2  25797  ellimc2  25912  limcflf  25916  lhop1lem  26052  lgsquadlem3  27426  rplogsum  27571  noextend  27711  noextendseq  27712  noetasuplem2  27779  noetainflem2  27783  madeval2  27892  umgrislfupgrlem  29139  spthispth  29744  cyclnumvtx  29820  0pth  30144  1pthdlem2  30155  frgrncvvdeqlem3  30320  ex-in  30444  chdmj3i  31502  chdmj4i  31503  chjassi  31505  pjoml2i  31604  pjoml3i  31605  cmcmlem  31610  cmcm2i  31612  cmbr3i  31619  fh3i  31642  fh4i  31643  osumcor2i  31663  mayetes3i  31748  mdslmd3i  32351  mdexchi  32354  atabsi  32420  dmdbr5ati  32441  inin  32535  uniin2  32565  of0r  32688  dfprm3  33581  ordtrest2NEW  33922  hasheuni  34086  carsgclctunlem1  34319  eulerpartgbij  34374  fiblem  34400  cvmscld  35278  sate0  35420  msrid  35550  elrn3  35762  bj-inrab3  36930  poimirlem15  37642  mblfinlem2  37665  ftc1anclem6  37705  xrnres2  38404  redundss3  38629  refrelsredund4  38633  pol0N  39911  readvrec2  42391  mapfzcons2  42730  diophrw  42770  conrel2d  43677  iunrelexp0  43715  hashnzfz  44339  wfaxpow  45014  disjinfi  45197  fourierdlem80  46201  sge0resplit  46421  sge0split  46424  caragenuncllem  46527  iscnrm3rlem1  48837