Theorem ineq2 4155

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

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3889

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897

This theorem is referenced by:  ineq12  4156  ineq2i  4158  ineq2d  4161  uneqin  4230  wefrc  5618  onfr  6356  onnseq  8277  qsdisj  8734  disjenex  9066  fiint  9230  elfiun  9336  dffi3  9337  cplem2  9805  dfac5  10042  kmlem2  10065  kmlem13  10076  kmlem14  10077  ackbij1lem16  10147  fin23lem12  10244  fin23lem19  10249  fin23lem33  10258  uzin2  15298  pgpfac1lem3  20045  pgpfac1lem5  20047  pgpfac1  20048  inopn  22874  basis1  22925  basis2  22926  baspartn  22929  fctop  22979  cctop  22981  ordtbaslem  23163  hausnei2  23328  cnhaus  23329  nrmsep  23332  isnrm2  23333  dishaus  23357  ordthauslem  23358  dfconn2  23394  nconnsubb  23398  finlocfin  23495  dissnlocfin  23504  locfindis  23505  kgeni  23512  pthaus  23613  txhaus  23622  xkohaus  23628  regr1lem  23714  fbasssin  23811  fbun  23815  fbunfip  23844  filconn  23858  isufil2  23883  ufileu  23894  filufint  23895  fmfnfmlem4  23932  fmfnfm  23933  fclsopni  23990  fclsbas  23996  fclsrest  23999  isfcf  24009  tsmsfbas  24103  ustincl  24183  ust0  24195  metreslem  24337  methaus  24495  qtopbaslem  24733  metnrmlem3  24837  ismbl  25503  shincl  31467  chincl  31585  chdmm1  31611  ledi  31626  cmbr  31670  cmbr3i  31686  cmbr3  31694  pjoml2  31697  stcltrlem1  32362  mdbr  32380  dmdbr  32385  cvmd  32422  cvexch  32460  sumdmdii  32501  mddmdin0i  32517  ofpreima2  32754  ssdifidllem  33531  ssdifidl  33532  ssdifidlprm  33533  1arithufdlem4  33622  crefeq  34005  ldgenpisyslem1  34323  ldgenpisys  34326  inelsros  34338  diffiunisros  34339  elcarsg  34465  carsgclctunlem2  34479  carsgclctun  34481  ballotlemfval  34650  ballotlemgval  34684  fineqvomon  35278  cvmscbv  35456  cvmsdisj  35468  cvmsss2  35472  satfv1  35561  nepss  35916  tailfb  36575  dfttc4lem1  36726  bj-0int  37429  mblfinlem2  37993  qsdisjALTV  39034  disjimeceqim  39139  lshpinN  39449  elrfi  43140  fipjust  44010  conrel1d  44108  ntrk0kbimka  44484  clsk3nimkb  44485  isotone2  44494  ntrclskb  44514  ntrclsk3  44515  ntrclsk13  44516  csbresgVD  45339  wfac8prim  45447  permac8prim  45459  disjf1  45631  qinioo  45983  fouriersw  46677  nnfoctbdjlem  46901  meadjun  46908  caragenel  46941  sepnsepolem2  49410  sepfsepc  49415  iscnrm3rlem8  49434  iscnrm3llem2  49437