Theorem ineq2 4154

Description: Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)

Assertion

Ref	Expression
ineq2	⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Proof of Theorem ineq2

Step	Hyp	Ref	Expression
1		ineq1 4153	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
2		incom 4149	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4149	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896

This theorem is referenced by:  ineq12  4155  ineq2i  4157  ineq2d  4160  uneqin  4229  wefrc  5625  onfr  6362  onnseq  8284  qsdisj  8741  disjenex  9073  fiint  9237  elfiun  9343  dffi3  9344  cplem2  9814  dfac5  10051  kmlem2  10074  kmlem13  10085  kmlem14  10086  ackbij1lem16  10156  fin23lem12  10253  fin23lem19  10258  fin23lem33  10267  uzin2  15307  pgpfac1lem3  20054  pgpfac1lem5  20056  pgpfac1  20057  inopn  22864  basis1  22915  basis2  22916  baspartn  22919  fctop  22969  cctop  22971  ordtbaslem  23153  hausnei2  23318  cnhaus  23319  nrmsep  23322  isnrm2  23323  dishaus  23347  ordthauslem  23348  dfconn2  23384  nconnsubb  23388  finlocfin  23485  dissnlocfin  23494  locfindis  23495  kgeni  23502  pthaus  23603  txhaus  23612  xkohaus  23618  regr1lem  23704  fbasssin  23801  fbun  23805  fbunfip  23834  filconn  23848  isufil2  23873  ufileu  23884  filufint  23885  fmfnfmlem4  23922  fmfnfm  23923  fclsopni  23980  fclsbas  23986  fclsrest  23989  isfcf  23999  tsmsfbas  24093  ustincl  24173  ust0  24185  metreslem  24327  methaus  24485  qtopbaslem  24723  metnrmlem3  24827  ismbl  25493  shincl  31452  chincl  31570  chdmm1  31596  ledi  31611  cmbr  31655  cmbr3i  31671  cmbr3  31679  pjoml2  31682  stcltrlem1  32347  mdbr  32365  dmdbr  32370  cvmd  32407  cvexch  32445  sumdmdii  32486  mddmdin0i  32502  ofpreima2  32739  ssdifidllem  33516  ssdifidl  33517  ssdifidlprm  33518  1arithufdlem4  33607  crefeq  33989  ldgenpisyslem1  34307  ldgenpisys  34310  inelsros  34322  diffiunisros  34323  elcarsg  34449  carsgclctunlem2  34463  carsgclctun  34465  ballotlemfval  34634  ballotlemgval  34668  fineqvomon  35262  cvmscbv  35440  cvmsdisj  35452  cvmsss2  35456  satfv1  35545  nepss  35900  tailfb  36559  dfttc4lem1  36710  bj-0int  37413  mblfinlem2  37979  qsdisjALTV  39020  disjimeceqim  39125  lshpinN  39435  elrfi  43126  fipjust  43992  conrel1d  44090  ntrk0kbimka  44466  clsk3nimkb  44467  isotone2  44476  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  csbresgVD  45321  wfac8prim  45429  permac8prim  45441  disjf1  45613  qinioo  45965  fouriersw  46659  nnfoctbdjlem  46883  meadjun  46890  caragenel  46923  sepnsepolem2  49398  sepfsepc  49403  iscnrm3rlem8  49422  iscnrm3llem2  49425