Theorem ineq2i 4074

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

Syntax hints:   = wceq 1507   ∩ cin 3829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-rab 3098  df-v 3418  df-in 3837

This theorem is referenced by:  in4  4090  inindir  4092  indif2  4135  difun1  4152  dfrab3ss  4169  undif1  4307  difdifdir  4320  dfif3  4364  dfif5  4366  disjpr2  4523  disjprsn  4524  disjtp2  4526  intunsn  4788  rint0  4789  riin0  4870  csbres  5698  res0  5699  resres  5711  resundi  5712  resindi  5714  inres  5716  resiun2  5719  resopab  5747  dffr3  5802  dfse2  5803  dminxp  5877  imainrect  5878  resdmres  5928  dfpred2  5995  predidm  6008  funimacnv  6268  fresaun  6378  fresaunres2  6379  wfrlem13  7771  tfrlem10  7827  sbthlem5  8427  infssuni  8610  dfsup2  8703  en3lplem2  8870  wemapwe  8954  epfrs  8967  r0weon  9232  infxpenlem  9233  kmlem11  9380  ackbij1lem1  9440  ackbij1lem2  9441  axdc3lem4  9673  canthwelem  9870  dmaddpi  10110  dmmulpi  10111  ssxr  10510  dmhashres  13516  fz1isolem  13632  f1oun2prg  14141  fsumiun  15036  sadeq  15681  bitsres  15682  smuval2  15691  smumul  15702  ressinbas  16416  lubdm  17447  glbdm  17460  sylow2a  18505  lsmmod2  18560  lsmdisj2r  18569  ablfac1eu  18945  ressmplbas2  19949  opsrtoslem1  19977  pjdm  20553  rintopn  21221  ordtrest2  21516  cmpsublem  21711  kgentopon  21850  hausdiag  21957  uzrest  22209  ufprim  22221  trust  22541  metnrmlem3  23172  clsocv  23556  ismbl  23830  unmbl  23841  volinun  23850  voliunlem1  23854  ovolioo  23872  itg2cnlem2  24066  ellimc2  24178  limcflf  24182  lhop1lem  24313  lgsquadlem3  25660  rplogsum  25805  umgrislfupgrlem  26610  spthispth  27215  0pth  27654  1pthdlem2  27665  frgrncvvdeqlem3  27835  ex-in  27982  chdmj3i  29041  chdmj4i  29042  chjassi  29044  pjoml2i  29143  pjoml3i  29144  cmcmlem  29149  cmcm2i  29151  cmbr3i  29158  fh3i  29181  fh4i  29182  osumcor2i  29202  mayetes3i  29287  mdslmd3i  29890  mdexchi  29893  atabsi  29959  dmdbr5ati  29980  inin  30053  uniin2  30072  ordtrest2NEW  30807  hasheuni  30985  carsgclctunlem1  31217  eulerpartgbij  31272  fiblem  31299  cvmscld  32102  msrid  32309  dfpo2  32508  elrn3  32515  noextend  32691  noextendseq  32692  madeval2  32808  bj-inrab3  33739  poimirlem15  34345  mblfinlem2  34368  ftc1anclem6  34410  xrnres2  35093  redundss3  35305  refrelsredund4  35309  pol0N  36487  mapfzcons2  38708  diophrw  38748  conrel2d  39369  iunrelexp0  39407  hashnzfz  40065  disjinfi  40876  fourierdlem80  41900  sge0resplit  42117  sge0split  42120  caragenuncllem  42223