Theorem ineq2 4194

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938

This theorem is referenced by:  ineq12  4195  ineq2i  4197  ineq2d  4200  uneqin  4269  wefrc  5653  onfr  6396  onnseq  8363  qsdisj  8813  disjenex  9154  fiint  9343  fiintOLD  9344  elfiun  9447  dffi3  9448  cplem2  9909  dfac5  10148  kmlem2  10171  kmlem13  10182  kmlem14  10183  ackbij1lem16  10253  fin23lem12  10350  fin23lem19  10355  fin23lem33  10364  uzin2  15368  pgpfac1lem3  20065  pgpfac1lem5  20067  pgpfac1  20068  inopn  22842  basis1  22893  basis2  22894  baspartn  22897  fctop  22947  cctop  22949  ordtbaslem  23131  hausnei2  23296  cnhaus  23297  nrmsep  23300  isnrm2  23301  dishaus  23325  ordthauslem  23326  dfconn2  23362  nconnsubb  23366  finlocfin  23463  dissnlocfin  23472  locfindis  23473  kgeni  23480  pthaus  23581  txhaus  23590  xkohaus  23596  regr1lem  23682  fbasssin  23779  fbun  23783  fbunfip  23812  filconn  23826  isufil2  23851  ufileu  23862  filufint  23863  fmfnfmlem4  23900  fmfnfm  23901  fclsopni  23958  fclsbas  23964  fclsrest  23967  isfcf  23977  tsmsfbas  24071  ustincl  24151  ust0  24163  metreslem  24306  methaus  24464  qtopbaslem  24702  metnrmlem3  24806  ismbl  25484  shincl  31367  chincl  31485  chdmm1  31511  ledi  31526  cmbr  31570  cmbr3i  31586  cmbr3  31594  pjoml2  31597  stcltrlem1  32262  mdbr  32280  dmdbr  32285  cvmd  32322  cvexch  32360  sumdmdii  32401  mddmdin0i  32417  ofpreima2  32649  ssdifidllem  33476  ssdifidl  33477  ssdifidlprm  33478  1arithufdlem4  33567  crefeq  33881  ldgenpisyslem1  34199  ldgenpisys  34202  inelsros  34214  diffiunisros  34215  elcarsg  34342  carsgclctunlem2  34356  carsgclctun  34358  ballotlemfval  34527  ballotlemgval  34561  cvmscbv  35285  cvmsdisj  35297  cvmsss2  35301  satfv1  35390  nepss  35740  tailfb  36400  bj-0int  37124  mblfinlem2  37687  qsdisjALTV  38638  lshpinN  39012  elrfi  42692  fipjust  43564  conrel1d  43662  ntrk0kbimka  44038  clsk3nimkb  44039  isotone2  44048  ntrclskb  44068  ntrclsk3  44069  ntrclsk13  44070  csbresgVD  44894  wfac8prim  45002  permac8prim  45014  disjf1  45187  qinioo  45544  fouriersw  46240  nnfoctbdjlem  46464  meadjun  46471  caragenel  46504  sepnsepolem2  48877  sepfsepc  48882  iscnrm3rlem8  48901  iscnrm3llem2  48904