Theorem ineq2 4121

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

Syntax hints:   → wi 4   = wceq 1543   ∩ cin 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-in 3873

This theorem is referenced by:  ineq12  4122  ineq2i  4124  ineq2d  4127  uneqin  4193  intprgOLD  4895  wefrc  5545  onfr  6252  onnseq  8081  qsdisj  8476  disjenex  8804  fiint  8948  elfiun  9046  dffi3  9047  cplem2  9506  dfac5  9742  kmlem2  9765  kmlem13  9776  kmlem14  9777  ackbij1lem16  9849  fin23lem12  9945  fin23lem19  9950  fin23lem33  9959  uzin2  14908  pgpfac1lem3  19464  pgpfac1lem5  19466  pgpfac1  19467  inopn  21796  basis1  21847  basis2  21848  baspartn  21851  fctop  21901  cctop  21903  ordtbaslem  22085  hausnei2  22250  cnhaus  22251  nrmsep  22254  isnrm2  22255  dishaus  22279  ordthauslem  22280  dfconn2  22316  nconnsubb  22320  finlocfin  22417  dissnlocfin  22426  locfindis  22427  kgeni  22434  pthaus  22535  txhaus  22544  xkohaus  22550  regr1lem  22636  fbasssin  22733  fbun  22737  fbunfip  22766  filconn  22780  isufil2  22805  ufileu  22816  filufint  22817  fmfnfmlem4  22854  fmfnfm  22855  fclsopni  22912  fclsbas  22918  fclsrest  22921  isfcf  22931  tsmsfbas  23025  ustincl  23105  ust0  23117  metreslem  23260  methaus  23418  qtopbaslem  23656  metnrmlem3  23758  ismbl  24423  shincl  29462  chincl  29580  chdmm1  29606  ledi  29621  cmbr  29665  cmbr3i  29681  cmbr3  29689  pjoml2  29692  stcltrlem1  30357  mdbr  30375  dmdbr  30380  cvmd  30417  cvexch  30455  sumdmdii  30496  mddmdin0i  30512  ofpreima2  30723  crefeq  31509  ldgenpisyslem1  31843  ldgenpisys  31846  inelsros  31858  diffiunisros  31859  elcarsg  31984  carsgclctunlem2  31998  carsgclctun  32000  ballotlemfval  32168  ballotlemgval  32202  cvmscbv  32933  cvmsdisj  32945  cvmsss2  32949  satfv1  33038  nepss  33377  tailfb  34303  bj-0int  35007  mblfinlem2  35552  qsdisjALTV  36465  lshpinN  36740  elrfi  40219  fipjust  40848  conrel1d  40948  ntrk0kbimka  41326  clsk3nimkb  41327  isotone2  41336  ntrclskb  41356  ntrclsk3  41357  ntrclsk13  41358  csbresgVD  42188  disjf1  42393  qinioo  42748  fouriersw  43447  nnfoctbdjlem  43668  meadjun  43675  caragenel  43708  sepnsepolem2  45889  sepfsepc  45894  iscnrm3rlem8  45914  iscnrm3llem2  45917