Theorem ineq2 4177

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

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

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 3406  df-in 3921

This theorem is referenced by:  ineq12  4178  ineq2i  4180  ineq2d  4183  uneqin  4252  wefrc  5632  onfr  6371  onnseq  8313  qsdisj  8767  disjenex  9099  fiint  9277  fiintOLD  9278  elfiun  9381  dffi3  9382  cplem2  9843  dfac5  10082  kmlem2  10105  kmlem13  10116  kmlem14  10117  ackbij1lem16  10187  fin23lem12  10284  fin23lem19  10289  fin23lem33  10298  uzin2  15311  pgpfac1lem3  20009  pgpfac1lem5  20011  pgpfac1  20012  inopn  22786  basis1  22837  basis2  22838  baspartn  22841  fctop  22891  cctop  22893  ordtbaslem  23075  hausnei2  23240  cnhaus  23241  nrmsep  23244  isnrm2  23245  dishaus  23269  ordthauslem  23270  dfconn2  23306  nconnsubb  23310  finlocfin  23407  dissnlocfin  23416  locfindis  23417  kgeni  23424  pthaus  23525  txhaus  23534  xkohaus  23540  regr1lem  23626  fbasssin  23723  fbun  23727  fbunfip  23756  filconn  23770  isufil2  23795  ufileu  23806  filufint  23807  fmfnfmlem4  23844  fmfnfm  23845  fclsopni  23902  fclsbas  23908  fclsrest  23911  isfcf  23921  tsmsfbas  24015  ustincl  24095  ust0  24107  metreslem  24250  methaus  24408  qtopbaslem  24646  metnrmlem3  24750  ismbl  25427  shincl  31310  chincl  31428  chdmm1  31454  ledi  31469  cmbr  31513  cmbr3i  31529  cmbr3  31537  pjoml2  31540  stcltrlem1  32205  mdbr  32223  dmdbr  32228  cvmd  32265  cvexch  32303  sumdmdii  32344  mddmdin0i  32360  ofpreima2  32590  ssdifidllem  33427  ssdifidl  33428  ssdifidlprm  33429  1arithufdlem4  33518  crefeq  33835  ldgenpisyslem1  34153  ldgenpisys  34156  inelsros  34168  diffiunisros  34169  elcarsg  34296  carsgclctunlem2  34310  carsgclctun  34312  ballotlemfval  34481  ballotlemgval  34515  cvmscbv  35245  cvmsdisj  35257  cvmsss2  35261  satfv1  35350  nepss  35705  tailfb  36365  bj-0int  37089  mblfinlem2  37652  qsdisjALTV  38606  lshpinN  38982  elrfi  42682  fipjust  43554  conrel1d  43652  ntrk0kbimka  44028  clsk3nimkb  44029  isotone2  44038  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  csbresgVD  44884  wfac8prim  44992  permac8prim  45004  disjf1  45177  qinioo  45533  fouriersw  46229  nnfoctbdjlem  46453  meadjun  46460  caragenel  46493  sepnsepolem2  48908  sepfsepc  48913  iscnrm3rlem8  48932  iscnrm3llem2  48935