Theorem ineq2 4160

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906

This theorem is used by:  ineq12  4161  ineq2i  4163  ineq2d  4166  uneqin  4235  wefrc  5645  onfr  6402  onnseq  8352  qsdisj  8815  disjenex  9154  fiint  9318  elfiun  9422  dffi3  9423  cplem2  9952  cplem2OLD  9953  dfac5  10207  kmlem2  10230  kmlem13  10241  kmlem14  10242  ackbij1lem16  10312  fin23lem12  10409  fin23lem19  10414  fin23lem33  10423  uzin2  15512  pgpfac1lem3  20293  pgpfac1lem5  20295  pgpfac1  20296  ssdifidllem  21640  ssdifidl  21641  ssdifidlprm  21642  inopn  23217  basis1  23268  basis2  23269  baspartn  23272  fctop  23322  cctop  23324  ordtbaslem  23506  hausnei2  23671  cnhaus  23672  nrmsep  23675  isnrm2  23676  dishaus  23700  ordthauslem  23701  dfconn2  23737  nconnsubb  23741  finlocfin  23839  dissnlocfin  23848  locfindis  23849  kgeni  23856  pthaus  23957  txhaus  23966  xkohaus  23972  regr1lem  24058  fbasssin  24155  fbun  24159  fbunfip  24188  filconn  24202  isufil2  24227  ufileu  24238  filufint  24239  fmfnfmlem4  24276  fmfnfm  24277  fclsopni  24334  fclsbas  24340  fclsrest  24343  isfcf  24353  tsmsfbas  24447  ustincl  24527  ust0  24539  metreslem  24681  methaus  24839  qtopbaslem  25077  metnrmlem3  25181  ismbl  25847  shincl  31983  chincl  32101  chdmm1  32127  ledi  32142  cmbr  32186  cmbr3i  32202  cmbr3  32210  pjoml2  32213  stcltrlem1  32878  mdbr  32896  dmdbr  32901  cvmd  32938  cvexch  32976  sumdmdii  33017  mddmdin0i  33033  ofpreima2  33260  1arithufdlem4  34079  crefeq  34477  ldgenpisyslem1  34796  ldgenpisys  34799  inelsros  34811  diffiunisros  34812  elcarsg  34937  carsgclctunlem2  34951  carsgclctun  34953  ballotlemfval  35122  ballotlemgval  35156  fineqvomon  35786  cvmscbv  36023  cvmsdisj  36035  cvmsss2  36039  satfv1  36128  nepss  36483  tailfb  37165  dfttc4lem1  37316  bj-0int  38022  mblfinlem2  38576  qsdisjALTV  39631  disjimeceqim  39736  lshpinN  40046  elrfi  43704  fipjust  44565  conrel1d  44662  ntrk0kbimka  45038  clsk3nimkb  45039  isotone2  45048  ntrclskb  45068  ntrclsk3  45069  ntrclsk13  45070  csbresgVD  45876  wfac8prim  45991  permac8prim  46003  disjf1  46197  qinioo  46546  fouriersw  47240  nnfoctbdjlem  47464  meadjun  47471  caragenel  47504  sepnsepolem2  50030  sepfsepc  50035  iscnrm3rlem8  50054  iscnrm3llem2  50057