Theorem ineq2 4141

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3895

This theorem is referenced by:  ineq12  4142  ineq2i  4144  ineq2d  4147  uneqin  4213  intprgOLD  4916  wefrc  5584  onfr  6309  onnseq  8184  qsdisj  8592  disjenex  8931  fiint  9100  elfiun  9198  dffi3  9199  cplem2  9657  dfac5  9893  kmlem2  9916  kmlem13  9927  kmlem14  9928  ackbij1lem16  10000  fin23lem12  10096  fin23lem19  10101  fin23lem33  10110  uzin2  15065  pgpfac1lem3  19689  pgpfac1lem5  19691  pgpfac1  19692  inopn  22057  basis1  22109  basis2  22110  baspartn  22113  fctop  22163  cctop  22165  ordtbaslem  22348  hausnei2  22513  cnhaus  22514  nrmsep  22517  isnrm2  22518  dishaus  22542  ordthauslem  22543  dfconn2  22579  nconnsubb  22583  finlocfin  22680  dissnlocfin  22689  locfindis  22690  kgeni  22697  pthaus  22798  txhaus  22807  xkohaus  22813  regr1lem  22899  fbasssin  22996  fbun  23000  fbunfip  23029  filconn  23043  isufil2  23068  ufileu  23079  filufint  23080  fmfnfmlem4  23117  fmfnfm  23118  fclsopni  23175  fclsbas  23181  fclsrest  23184  isfcf  23194  tsmsfbas  23288  ustincl  23368  ust0  23380  metreslem  23524  methaus  23685  qtopbaslem  23931  metnrmlem3  24033  ismbl  24699  shincl  29752  chincl  29870  chdmm1  29896  ledi  29911  cmbr  29955  cmbr3i  29971  cmbr3  29979  pjoml2  29982  stcltrlem1  30647  mdbr  30665  dmdbr  30670  cvmd  30707  cvexch  30745  sumdmdii  30786  mddmdin0i  30802  ofpreima2  31012  crefeq  31804  ldgenpisyslem1  32140  ldgenpisys  32143  inelsros  32155  diffiunisros  32156  elcarsg  32281  carsgclctunlem2  32295  carsgclctun  32297  ballotlemfval  32465  ballotlemgval  32499  cvmscbv  33229  cvmsdisj  33241  cvmsss2  33245  satfv1  33334  nepss  33671  tailfb  34575  bj-0int  35281  mblfinlem2  35824  qsdisjALTV  36735  lshpinN  37010  elrfi  40523  fipjust  41179  conrel1d  41278  ntrk0kbimka  41656  clsk3nimkb  41657  isotone2  41666  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  csbresgVD  42522  disjf1  42727  qinioo  43080  fouriersw  43779  nnfoctbdjlem  44000  meadjun  44007  caragenel  44040  sepnsepolem2  46227  sepfsepc  46232  iscnrm3rlem8  46252  iscnrm3llem2  46255