Theorem ineq2 4168

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

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

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 3402  df-in 3910

This theorem is referenced by:  ineq12  4169  ineq2i  4171  ineq2d  4174  uneqin  4243  wefrc  5626  onfr  6364  onnseq  8286  qsdisj  8743  disjenex  9075  fiint  9239  elfiun  9345  dffi3  9346  cplem2  9814  dfac5  10051  kmlem2  10074  kmlem13  10085  kmlem14  10086  ackbij1lem16  10156  fin23lem12  10253  fin23lem19  10258  fin23lem33  10267  uzin2  15280  pgpfac1lem3  20020  pgpfac1lem5  20022  pgpfac1  20023  inopn  22855  basis1  22906  basis2  22907  baspartn  22910  fctop  22960  cctop  22962  ordtbaslem  23144  hausnei2  23309  cnhaus  23310  nrmsep  23313  isnrm2  23314  dishaus  23338  ordthauslem  23339  dfconn2  23375  nconnsubb  23379  finlocfin  23476  dissnlocfin  23485  locfindis  23486  kgeni  23493  pthaus  23594  txhaus  23603  xkohaus  23609  regr1lem  23695  fbasssin  23792  fbun  23796  fbunfip  23825  filconn  23839  isufil2  23864  ufileu  23875  filufint  23876  fmfnfmlem4  23913  fmfnfm  23914  fclsopni  23971  fclsbas  23977  fclsrest  23980  isfcf  23990  tsmsfbas  24084  ustincl  24164  ust0  24176  metreslem  24318  methaus  24476  qtopbaslem  24714  metnrmlem3  24818  ismbl  25495  shincl  31469  chincl  31587  chdmm1  31613  ledi  31628  cmbr  31672  cmbr3i  31688  cmbr3  31696  pjoml2  31699  stcltrlem1  32364  mdbr  32382  dmdbr  32387  cvmd  32424  cvexch  32462  sumdmdii  32503  mddmdin0i  32519  ofpreima2  32756  ssdifidllem  33549  ssdifidl  33550  ssdifidlprm  33551  1arithufdlem4  33640  crefeq  34023  ldgenpisyslem1  34341  ldgenpisys  34344  inelsros  34356  diffiunisros  34357  elcarsg  34483  carsgclctunlem2  34497  carsgclctun  34499  ballotlemfval  34668  ballotlemgval  34702  fineqvomon  35296  cvmscbv  35474  cvmsdisj  35486  cvmsss2  35490  satfv1  35579  nepss  35934  tailfb  36593  bj-0int  37354  mblfinlem2  37909  qsdisjALTV  38950  disjimeceqim  39055  lshpinN  39365  elrfi  43051  fipjust  43921  conrel1d  44019  ntrk0kbimka  44395  clsk3nimkb  44396  isotone2  44405  ntrclskb  44425  ntrclsk3  44426  ntrclsk13  44427  csbresgVD  45250  wfac8prim  45358  permac8prim  45370  disjf1  45542  qinioo  45895  fouriersw  46589  nnfoctbdjlem  46813  meadjun  46820  caragenel  46853  sepnsepolem2  49282  sepfsepc  49287  iscnrm3rlem8  49306  iscnrm3llem2  49309