Theorem ineq2 4205

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

Syntax hints:   → wi 4   = wceq 1541   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3954

This theorem is referenced by:  ineq12  4206  ineq2i  4208  ineq2d  4211  uneqin  4277  intprgOLD  4987  wefrc  5669  onfr  6400  onnseq  8340  qsdisj  8784  disjenex  9131  fiint  9320  elfiun  9421  dffi3  9422  cplem2  9881  dfac5  10119  kmlem2  10142  kmlem13  10153  kmlem14  10154  ackbij1lem16  10226  fin23lem12  10322  fin23lem19  10327  fin23lem33  10336  uzin2  15287  pgpfac1lem3  19941  pgpfac1lem5  19943  pgpfac1  19944  inopn  22392  basis1  22444  basis2  22445  baspartn  22448  fctop  22498  cctop  22500  ordtbaslem  22683  hausnei2  22848  cnhaus  22849  nrmsep  22852  isnrm2  22853  dishaus  22877  ordthauslem  22878  dfconn2  22914  nconnsubb  22918  finlocfin  23015  dissnlocfin  23024  locfindis  23025  kgeni  23032  pthaus  23133  txhaus  23142  xkohaus  23148  regr1lem  23234  fbasssin  23331  fbun  23335  fbunfip  23364  filconn  23378  isufil2  23403  ufileu  23414  filufint  23415  fmfnfmlem4  23452  fmfnfm  23453  fclsopni  23510  fclsbas  23516  fclsrest  23519  isfcf  23529  tsmsfbas  23623  ustincl  23703  ust0  23715  metreslem  23859  methaus  24020  qtopbaslem  24266  metnrmlem3  24368  ismbl  25034  shincl  30621  chincl  30739  chdmm1  30765  ledi  30780  cmbr  30824  cmbr3i  30840  cmbr3  30848  pjoml2  30851  stcltrlem1  31516  mdbr  31534  dmdbr  31539  cvmd  31576  cvexch  31614  sumdmdii  31655  mddmdin0i  31671  ofpreima2  31878  crefeq  32813  ldgenpisyslem1  33149  ldgenpisys  33152  inelsros  33164  diffiunisros  33165  elcarsg  33292  carsgclctunlem2  33306  carsgclctun  33308  ballotlemfval  33476  ballotlemgval  33510  cvmscbv  34237  cvmsdisj  34249  cvmsss2  34253  satfv1  34342  nepss  34675  tailfb  35250  bj-0int  35970  mblfinlem2  36514  qsdisjALTV  37473  lshpinN  37847  elrfi  41417  fipjust  42301  conrel1d  42399  ntrk0kbimka  42775  clsk3nimkb  42776  isotone2  42785  ntrclskb  42805  ntrclsk3  42806  ntrclsk13  42807  csbresgVD  43641  disjf1  43865  qinioo  44234  fouriersw  44933  nnfoctbdjlem  45157  meadjun  45164  caragenel  45197  sepnsepolem2  47508  sepfsepc  47513  iscnrm3rlem8  47533  iscnrm3llem2  47536