Theorem ineq2 4161

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 4160	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
2		incom 4156	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4156	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3eqtr4g 2791	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   = 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:  ineq12  4162  ineq2i  4164  ineq2d  4167  uneqin  4236  wefrc  5608  onfr  6345  onnseq  8264  qsdisj  8718  disjenex  9048  fiint  9211  elfiun  9314  dffi3  9315  cplem2  9783  dfac5  10020  kmlem2  10043  kmlem13  10054  kmlem14  10055  ackbij1lem16  10125  fin23lem12  10222  fin23lem19  10227  fin23lem33  10236  uzin2  15252  pgpfac1lem3  19991  pgpfac1lem5  19993  pgpfac1  19994  inopn  22814  basis1  22865  basis2  22866  baspartn  22869  fctop  22919  cctop  22921  ordtbaslem  23103  hausnei2  23268  cnhaus  23269  nrmsep  23272  isnrm2  23273  dishaus  23297  ordthauslem  23298  dfconn2  23334  nconnsubb  23338  finlocfin  23435  dissnlocfin  23444  locfindis  23445  kgeni  23452  pthaus  23553  txhaus  23562  xkohaus  23568  regr1lem  23654  fbasssin  23751  fbun  23755  fbunfip  23784  filconn  23798  isufil2  23823  ufileu  23834  filufint  23835  fmfnfmlem4  23872  fmfnfm  23873  fclsopni  23930  fclsbas  23936  fclsrest  23939  isfcf  23949  tsmsfbas  24043  ustincl  24123  ust0  24135  metreslem  24277  methaus  24435  qtopbaslem  24673  metnrmlem3  24777  ismbl  25454  shincl  31361  chincl  31479  chdmm1  31505  ledi  31520  cmbr  31564  cmbr3i  31580  cmbr3  31588  pjoml2  31591  stcltrlem1  32256  mdbr  32274  dmdbr  32279  cvmd  32316  cvexch  32354  sumdmdii  32395  mddmdin0i  32411  ofpreima2  32648  ssdifidllem  33421  ssdifidl  33422  ssdifidlprm  33423  1arithufdlem4  33512  crefeq  33858  ldgenpisyslem1  34176  ldgenpisys  34179  inelsros  34191  diffiunisros  34192  elcarsg  34318  carsgclctunlem2  34332  carsgclctun  34334  ballotlemfval  34503  ballotlemgval  34537  fineqvomon  35134  cvmscbv  35302  cvmsdisj  35314  cvmsss2  35318  satfv1  35407  nepss  35762  tailfb  36421  bj-0int  37145  mblfinlem2  37708  qsdisjALTV  38721  lshpinN  39098  elrfi  42797  fipjust  43668  conrel1d  43766  ntrk0kbimka  44142  clsk3nimkb  44143  isotone2  44152  ntrclskb  44172  ntrclsk3  44173  ntrclsk13  44174  csbresgVD  44997  wfac8prim  45105  permac8prim  45117  disjf1  45290  qinioo  45645  fouriersw  46339  nnfoctbdjlem  46563  meadjun  46570  caragenel  46603  sepnsepolem2  49033  sepfsepc  49038  iscnrm3rlem8  49057  iscnrm3llem2  49060