Theorem ineq2 4166

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

Syntax hints:   → wi 4   = wceq 1560   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3911

This theorem is referenced by:  ineq12  4167  ineq2i  4169  ineq2d  4172  uneqin  4241  wefrc  5641  onfr  6385  onnseq  8315  qsdisj  8776  disjenex  9107  fiint  9271  elfiun  9376  dffi3  9377  cplem2  9848  dfac5  10085  kmlem2  10108  kmlem13  10119  kmlem14  10120  ackbij1lem16  10190  fin23lem12  10288  fin23lem19  10293  fin23lem33  10302  uzin2  15372  pgpfac1lem3  20119  pgpfac1lem5  20121  pgpfac1  20122  inopn  22959  basis1  23010  basis2  23011  baspartn  23014  fctop  23064  cctop  23066  ordtbaslem  23248  hausnei2  23413  cnhaus  23414  nrmsep  23417  isnrm2  23418  dishaus  23442  ordthauslem  23443  dfconn2  23479  nconnsubb  23483  finlocfin  23580  dissnlocfin  23589  locfindis  23590  kgeni  23597  pthaus  23698  txhaus  23707  xkohaus  23713  regr1lem  23799  fbasssin  23896  fbun  23900  fbunfip  23929  filconn  23943  isufil2  23968  ufileu  23979  filufint  23980  fmfnfmlem4  24017  fmfnfm  24018  fclsopni  24075  fclsbas  24081  fclsrest  24084  isfcf  24094  tsmsfbas  24188  ustincl  24268  ust0  24280  metreslem  24422  methaus  24580  qtopbaslem  24818  metnrmlem3  24922  ismbl  25588  shincl  31584  chincl  31702  chdmm1  31728  ledi  31743  cmbr  31787  cmbr3i  31803  cmbr3  31811  pjoml2  31814  stcltrlem1  32479  mdbr  32497  dmdbr  32502  cvmd  32539  cvexch  32577  sumdmdii  32618  mddmdin0i  32634  ofpreima2  32868  ssdifidllem  33643  ssdifidl  33644  ssdifidlprm  33645  1arithufdlem4  33743  crefeq  34142  ldgenpisyslem1  34460  ldgenpisys  34463  inelsros  34475  diffiunisros  34476  elcarsg  34602  carsgclctunlem2  34616  carsgclctun  34618  ballotlemfval  34787  ballotlemgval  34821  fineqvomon  35414  cvmscbv  35608  cvmsdisj  35620  cvmsss2  35624  satfv1  35713  nepss  36068  tailfb  36737  dfttc4lem1  36888  bj-0int  37591  mblfinlem2  38157  qsdisjALTV  39198  disjimeceqim  39303  lshpinN  39613  elrfi  43275  fipjust  44141  conrel1d  44239  ntrk0kbimka  44615  clsk3nimkb  44616  isotone2  44625  ntrclskb  44645  ntrclsk3  44646  ntrclsk13  44647  csbresgVD  45470  wfac8prim  45578  permac8prim  45590  disjf1  45761  qinioo  46111  fouriersw  46805  nnfoctbdjlem  47029  meadjun  47036  caragenel  47069  sepnsepolem2  49544  sepfsepc  49549  iscnrm3rlem8  49568  iscnrm3llem2  49571