Theorem ineq2 4165

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-in 3910

This theorem is referenced by:  ineq12  4166  ineq2i  4168  ineq2d  4171  uneqin  4240  wefrc  5613  onfr  6346  onnseq  8267  qsdisj  8721  disjenex  9052  fiint  9216  fiintOLD  9217  elfiun  9320  dffi3  9321  cplem2  9786  dfac5  10023  kmlem2  10046  kmlem13  10057  kmlem14  10058  ackbij1lem16  10128  fin23lem12  10225  fin23lem19  10230  fin23lem33  10239  uzin2  15252  pgpfac1lem3  19958  pgpfac1lem5  19960  pgpfac1  19961  inopn  22784  basis1  22835  basis2  22836  baspartn  22839  fctop  22889  cctop  22891  ordtbaslem  23073  hausnei2  23238  cnhaus  23239  nrmsep  23242  isnrm2  23243  dishaus  23267  ordthauslem  23268  dfconn2  23304  nconnsubb  23308  finlocfin  23405  dissnlocfin  23414  locfindis  23415  kgeni  23422  pthaus  23523  txhaus  23532  xkohaus  23538  regr1lem  23624  fbasssin  23721  fbun  23725  fbunfip  23754  filconn  23768  isufil2  23793  ufileu  23804  filufint  23805  fmfnfmlem4  23842  fmfnfm  23843  fclsopni  23900  fclsbas  23906  fclsrest  23909  isfcf  23919  tsmsfbas  24013  ustincl  24093  ust0  24105  metreslem  24248  methaus  24406  qtopbaslem  24644  metnrmlem3  24748  ismbl  25425  shincl  31325  chincl  31443  chdmm1  31469  ledi  31484  cmbr  31528  cmbr3i  31544  cmbr3  31552  pjoml2  31555  stcltrlem1  32220  mdbr  32238  dmdbr  32243  cvmd  32280  cvexch  32318  sumdmdii  32359  mddmdin0i  32375  ofpreima2  32610  ssdifidllem  33394  ssdifidl  33395  ssdifidlprm  33396  1arithufdlem4  33485  crefeq  33818  ldgenpisyslem1  34136  ldgenpisys  34139  inelsros  34151  diffiunisros  34152  elcarsg  34279  carsgclctunlem2  34293  carsgclctun  34295  ballotlemfval  34464  ballotlemgval  34498  cvmscbv  35241  cvmsdisj  35253  cvmsss2  35257  satfv1  35346  nepss  35701  tailfb  36361  bj-0int  37085  mblfinlem2  37648  qsdisjALTV  38602  lshpinN  38978  elrfi  42677  fipjust  43548  conrel1d  43646  ntrk0kbimka  44022  clsk3nimkb  44023  isotone2  44032  ntrclskb  44052  ntrclsk3  44053  ntrclsk13  44054  csbresgVD  44878  wfac8prim  44986  permac8prim  44998  disjf1  45171  qinioo  45526  fouriersw  46222  nnfoctbdjlem  46446  meadjun  46453  caragenel  46486  sepnsepolem2  48917  sepfsepc  48922  iscnrm3rlem8  48941  iscnrm3llem2  48944