Theorem ineq2 4155

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897

This theorem is referenced by:  ineq12  4156  ineq2i  4158  ineq2d  4161  uneqin  4230  wefrc  5619  onfr  6357  onnseq  8278  qsdisj  8735  disjenex  9067  fiint  9231  elfiun  9337  dffi3  9338  cplem2  9808  dfac5  10045  kmlem2  10068  kmlem13  10079  kmlem14  10080  ackbij1lem16  10150  fin23lem12  10247  fin23lem19  10252  fin23lem33  10261  uzin2  15301  pgpfac1lem3  20048  pgpfac1lem5  20050  pgpfac1  20051  inopn  22877  basis1  22928  basis2  22929  baspartn  22932  fctop  22982  cctop  22984  ordtbaslem  23166  hausnei2  23331  cnhaus  23332  nrmsep  23335  isnrm2  23336  dishaus  23360  ordthauslem  23361  dfconn2  23397  nconnsubb  23401  finlocfin  23498  dissnlocfin  23507  locfindis  23508  kgeni  23515  pthaus  23616  txhaus  23625  xkohaus  23631  regr1lem  23717  fbasssin  23814  fbun  23818  fbunfip  23847  filconn  23861  isufil2  23886  ufileu  23897  filufint  23898  fmfnfmlem4  23935  fmfnfm  23936  fclsopni  23993  fclsbas  23999  fclsrest  24002  isfcf  24012  tsmsfbas  24106  ustincl  24186  ust0  24198  metreslem  24340  methaus  24498  qtopbaslem  24736  metnrmlem3  24840  ismbl  25506  shincl  31470  chincl  31588  chdmm1  31614  ledi  31629  cmbr  31673  cmbr3i  31689  cmbr3  31697  pjoml2  31700  stcltrlem1  32365  mdbr  32383  dmdbr  32388  cvmd  32425  cvexch  32463  sumdmdii  32504  mddmdin0i  32520  ofpreima2  32757  ssdifidllem  33534  ssdifidl  33535  ssdifidlprm  33536  1arithufdlem4  33625  crefeq  34008  ldgenpisyslem1  34326  ldgenpisys  34329  inelsros  34341  diffiunisros  34342  elcarsg  34468  carsgclctunlem2  34482  carsgclctun  34484  ballotlemfval  34653  ballotlemgval  34687  fineqvomon  35281  cvmscbv  35459  cvmsdisj  35471  cvmsss2  35475  satfv1  35564  nepss  35919  tailfb  36578  dfttc4lem1  36729  bj-0int  37432  mblfinlem2  37996  qsdisjALTV  39037  disjimeceqim  39142  lshpinN  39452  elrfi  43143  fipjust  44013  conrel1d  44111  ntrk0kbimka  44487  clsk3nimkb  44488  isotone2  44497  ntrclskb  44517  ntrclsk3  44518  ntrclsk13  44519  csbresgVD  45342  wfac8prim  45450  permac8prim  45462  disjf1  45634  qinioo  45986  fouriersw  46680  nnfoctbdjlem  46904  meadjun  46911  caragenel  46944  sepnsepolem2  49413  sepfsepc  49418  iscnrm3rlem8  49437  iscnrm3llem2  49440