Theorem ineq2 4137

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

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890

This theorem is referenced by:  ineq12  4138  ineq2i  4140  ineq2d  4143  uneqin  4209  intprgOLD  4912  wefrc  5574  onfr  6290  onnseq  8146  qsdisj  8541  disjenex  8871  fiint  9021  elfiun  9119  dffi3  9120  cplem2  9579  dfac5  9815  kmlem2  9838  kmlem13  9849  kmlem14  9850  ackbij1lem16  9922  fin23lem12  10018  fin23lem19  10023  fin23lem33  10032  uzin2  14984  pgpfac1lem3  19595  pgpfac1lem5  19597  pgpfac1  19598  inopn  21956  basis1  22008  basis2  22009  baspartn  22012  fctop  22062  cctop  22064  ordtbaslem  22247  hausnei2  22412  cnhaus  22413  nrmsep  22416  isnrm2  22417  dishaus  22441  ordthauslem  22442  dfconn2  22478  nconnsubb  22482  finlocfin  22579  dissnlocfin  22588  locfindis  22589  kgeni  22596  pthaus  22697  txhaus  22706  xkohaus  22712  regr1lem  22798  fbasssin  22895  fbun  22899  fbunfip  22928  filconn  22942  isufil2  22967  ufileu  22978  filufint  22979  fmfnfmlem4  23016  fmfnfm  23017  fclsopni  23074  fclsbas  23080  fclsrest  23083  isfcf  23093  tsmsfbas  23187  ustincl  23267  ust0  23279  metreslem  23423  methaus  23582  qtopbaslem  23828  metnrmlem3  23930  ismbl  24595  shincl  29644  chincl  29762  chdmm1  29788  ledi  29803  cmbr  29847  cmbr3i  29863  cmbr3  29871  pjoml2  29874  stcltrlem1  30539  mdbr  30557  dmdbr  30562  cvmd  30599  cvexch  30637  sumdmdii  30678  mddmdin0i  30694  ofpreima2  30905  crefeq  31697  ldgenpisyslem1  32031  ldgenpisys  32034  inelsros  32046  diffiunisros  32047  elcarsg  32172  carsgclctunlem2  32186  carsgclctun  32188  ballotlemfval  32356  ballotlemgval  32390  cvmscbv  33120  cvmsdisj  33132  cvmsss2  33136  satfv1  33225  nepss  33564  tailfb  34493  bj-0int  35199  mblfinlem2  35742  qsdisjALTV  36655  lshpinN  36930  elrfi  40432  fipjust  41061  conrel1d  41160  ntrk0kbimka  41538  clsk3nimkb  41539  isotone2  41548  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  csbresgVD  42404  disjf1  42609  qinioo  42963  fouriersw  43662  nnfoctbdjlem  43883  meadjun  43890  caragenel  43923  sepnsepolem2  46104  sepfsepc  46109  iscnrm3rlem8  46129  iscnrm3llem2  46132