Theorem ineq2 4182

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

Syntax hints:   → wi 4   = wceq 1533   ∩ cin 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1536  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3942

This theorem is referenced by:  ineq12  4183  ineq2i  4185  ineq2d  4188  uneqin  4254  intprg  4909  wefrc  5548  onfr  6229  onnseq  7980  qsdisj  8373  disjenex  8674  fiint  8794  elfiun  8893  dffi3  8894  cplem2  9318  dfac5  9553  kmlem2  9576  kmlem13  9587  kmlem14  9588  ackbij1lem16  9656  fin23lem12  9752  fin23lem19  9757  fin23lem33  9766  uzin2  14703  pgpfac1lem3  19198  pgpfac1lem5  19200  pgpfac1  19201  inopn  21506  basis1  21557  basis2  21558  baspartn  21561  fctop  21611  cctop  21613  ordtbaslem  21795  hausnei2  21960  cnhaus  21961  nrmsep  21964  isnrm2  21965  dishaus  21989  ordthauslem  21990  dfconn2  22026  nconnsubb  22030  finlocfin  22127  dissnlocfin  22136  locfindis  22137  kgeni  22144  pthaus  22245  txhaus  22254  xkohaus  22260  regr1lem  22346  fbasssin  22443  fbun  22447  fbunfip  22476  filconn  22490  isufil2  22515  ufileu  22526  filufint  22527  fmfnfmlem4  22564  fmfnfm  22565  fclsopni  22622  fclsbas  22628  fclsrest  22631  isfcf  22641  tsmsfbas  22735  ustincl  22815  ust0  22827  metreslem  22971  methaus  23129  qtopbaslem  23366  metnrmlem3  23468  ismbl  24126  shincl  29157  chincl  29275  chdmm1  29301  ledi  29316  cmbr  29360  cmbr3i  29376  cmbr3  29384  pjoml2  29387  stcltrlem1  30052  mdbr  30070  dmdbr  30075  cvmd  30112  cvexch  30150  sumdmdii  30191  mddmdin0i  30207  ofpreima2  30410  crefeq  31109  ldgenpisyslem1  31422  ldgenpisys  31425  inelsros  31437  diffiunisros  31438  elcarsg  31563  carsgclctunlem2  31577  carsgclctun  31579  ballotlemfval  31747  ballotlemgval  31781  cvmscbv  32505  cvmsdisj  32517  cvmsss2  32521  satfv1  32610  nepss  32948  tailfb  33725  bj-0int  34392  mblfinlem2  34929  qsdisjALTV  35849  lshpinN  36124  elrfi  39289  fipjust  39922  conrel1d  40006  ntrk0kbimka  40387  clsk3nimkb  40388  isotone2  40397  ntrclskb  40417  ntrclsk3  40418  ntrclsk13  40419  csbresgVD  41227  disjf1  41441  qinioo  41809  fouriersw  42515  nnfoctbdjlem  42736  meadjun  42743  caragenel  42776