Theorem ineq2 4173

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-in 3918

This theorem is referenced by:  ineq12  4174  ineq2i  4176  ineq2d  4179  uneqin  4248  wefrc  5625  onfr  6359  onnseq  8290  qsdisj  8744  disjenex  9076  fiint  9253  fiintOLD  9254  elfiun  9357  dffi3  9358  cplem2  9819  dfac5  10058  kmlem2  10081  kmlem13  10092  kmlem14  10093  ackbij1lem16  10163  fin23lem12  10260  fin23lem19  10265  fin23lem33  10274  uzin2  15287  pgpfac1lem3  19993  pgpfac1lem5  19995  pgpfac1  19996  inopn  22819  basis1  22870  basis2  22871  baspartn  22874  fctop  22924  cctop  22926  ordtbaslem  23108  hausnei2  23273  cnhaus  23274  nrmsep  23277  isnrm2  23278  dishaus  23302  ordthauslem  23303  dfconn2  23339  nconnsubb  23343  finlocfin  23440  dissnlocfin  23449  locfindis  23450  kgeni  23457  pthaus  23558  txhaus  23567  xkohaus  23573  regr1lem  23659  fbasssin  23756  fbun  23760  fbunfip  23789  filconn  23803  isufil2  23828  ufileu  23839  filufint  23840  fmfnfmlem4  23877  fmfnfm  23878  fclsopni  23935  fclsbas  23941  fclsrest  23944  isfcf  23954  tsmsfbas  24048  ustincl  24128  ust0  24140  metreslem  24283  methaus  24441  qtopbaslem  24679  metnrmlem3  24783  ismbl  25460  shincl  31360  chincl  31478  chdmm1  31504  ledi  31519  cmbr  31563  cmbr3i  31579  cmbr3  31587  pjoml2  31590  stcltrlem1  32255  mdbr  32273  dmdbr  32278  cvmd  32315  cvexch  32353  sumdmdii  32394  mddmdin0i  32410  ofpreima2  32640  ssdifidllem  33420  ssdifidl  33421  ssdifidlprm  33422  1arithufdlem4  33511  crefeq  33828  ldgenpisyslem1  34146  ldgenpisys  34149  inelsros  34161  diffiunisros  34162  elcarsg  34289  carsgclctunlem2  34303  carsgclctun  34305  ballotlemfval  34474  ballotlemgval  34508  cvmscbv  35238  cvmsdisj  35250  cvmsss2  35254  satfv1  35343  nepss  35698  tailfb  36358  bj-0int  37082  mblfinlem2  37645  qsdisjALTV  38599  lshpinN  38975  elrfi  42675  fipjust  43547  conrel1d  43645  ntrk0kbimka  44021  clsk3nimkb  44022  isotone2  44031  ntrclskb  44051  ntrclsk3  44052  ntrclsk13  44053  csbresgVD  44877  wfac8prim  44985  permac8prim  44997  disjf1  45170  qinioo  45526  fouriersw  46222  nnfoctbdjlem  46446  meadjun  46453  caragenel  46486  sepnsepolem2  48904  sepfsepc  48909  iscnrm3rlem8  48928  iscnrm3llem2  48931