Theorem ineq2 4103

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

Syntax hints:   → wi 4   = wceq 1522   ∩ cin 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-in 3866

This theorem is referenced by:  ineq12  4104  ineq2i  4106  ineq2d  4109  uneqin  4175  intprg  4816  wefrc  5437  onfr  6105  onnseq  7833  qsdisj  8224  disjenex  8522  fiint  8641  elfiun  8740  dffi3  8741  cplem2  9165  dfac5  9400  kmlem2  9423  kmlem13  9434  kmlem14  9435  ackbij1lem16  9503  fin23lem12  9599  fin23lem19  9604  fin23lem33  9613  uzin2  14538  pgpfac1lem3  18916  pgpfac1lem5  18918  pgpfac1  18919  inopn  21191  basis1  21242  basis2  21243  baspartn  21246  fctop  21296  cctop  21298  ordtbaslem  21480  hausnei2  21645  cnhaus  21646  nrmsep  21649  isnrm2  21650  dishaus  21674  ordthauslem  21675  dfconn2  21711  nconnsubb  21715  finlocfin  21812  dissnlocfin  21821  locfindis  21822  kgeni  21829  pthaus  21930  txhaus  21939  xkohaus  21945  regr1lem  22031  fbasssin  22128  fbun  22132  fbunfip  22161  filconn  22175  isufil2  22200  ufileu  22211  filufint  22212  fmfnfmlem4  22249  fmfnfm  22250  fclsopni  22307  fclsbas  22313  fclsrest  22316  isfcf  22326  tsmsfbas  22419  ustincl  22499  ust0  22511  metreslem  22655  methaus  22813  qtopbaslem  23050  metnrmlem3  23152  ismbl  23810  shincl  28849  chincl  28967  chdmm1  28993  ledi  29008  cmbr  29052  cmbr3i  29068  cmbr3  29076  pjoml2  29079  stcltrlem1  29744  mdbr  29762  dmdbr  29767  cvmd  29804  cvexch  29842  sumdmdii  29883  mddmdin0i  29899  ofpreima2  30101  crefeq  30726  ldgenpisyslem1  31039  ldgenpisys  31042  inelsros  31054  diffiunisros  31055  elcarsg  31180  carsgclctunlem2  31194  carsgclctun  31196  ballotlemfval  31364  ballotlemgval  31398  cvmscbv  32113  cvmsdisj  32125  cvmsss2  32129  satfv1  32218  nepss  32556  tailfb  33334  bj-0int  33992  mblfinlem2  34461  qsdisjALTV  35381  lshpinN  35656  elrfi  38776  fipjust  39409  conrel1d  39493  ntrk0kbimka  39874  clsk3nimkb  39875  isotone2  39884  ntrclskb  39904  ntrclsk3  39905  ntrclsk13  39906  csbresgVD  40768  disjf1  40983  qinioo  41353  fouriersw  42058  nnfoctbdjlem  42279  meadjun  42286  caragenel  42319