Theorem ineq2 4167

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

Syntax hints:   → wi 4   = wceq 1570   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3912

This theorem is referenced by:  ineq12  4168  ineq2i  4170  ineq2d  4173  uneqin  4242  wefrc  5655  onfr  6400  onnseq  8327  qsdisj  8788  disjenex  9119  fiint  9282  elfiun  9386  dffi3  9387  cplem2  9872  dfac5  10108  kmlem2  10131  kmlem13  10142  kmlem14  10143  ackbij1lem16  10213  fin23lem12  10310  fin23lem19  10315  fin23lem33  10324  uzin2  15392  pgpfac1lem3  20144  pgpfac1lem5  20146  pgpfac1  20147  ssdifidllem  21484  ssdifidl  21485  ssdifidlprm  21486  inopn  23056  basis1  23107  basis2  23108  baspartn  23111  fctop  23161  cctop  23163  ordtbaslem  23345  hausnei2  23510  cnhaus  23511  nrmsep  23514  isnrm2  23515  dishaus  23539  ordthauslem  23540  dfconn2  23576  nconnsubb  23580  finlocfin  23677  dissnlocfin  23686  locfindis  23687  kgeni  23694  pthaus  23795  txhaus  23804  xkohaus  23810  regr1lem  23896  fbasssin  23993  fbun  23997  fbunfip  24026  filconn  24040  isufil2  24065  ufileu  24076  filufint  24077  fmfnfmlem4  24114  fmfnfm  24115  fclsopni  24172  fclsbas  24178  fclsrest  24181  isfcf  24191  tsmsfbas  24285  ustincl  24365  ust0  24377  metreslem  24519  methaus  24677  qtopbaslem  24915  metnrmlem3  25019  ismbl  25685  shincl  31733  chincl  31851  chdmm1  31877  ledi  31892  cmbr  31936  cmbr3i  31952  cmbr3  31960  pjoml2  31963  stcltrlem1  32628  mdbr  32646  dmdbr  32651  cvmd  32688  cvexch  32726  sumdmdii  32767  mddmdin0i  32783  ofpreima2  33011  1arithufdlem4  33837  crefeq  34235  ldgenpisyslem1  34553  ldgenpisys  34556  inelsros  34568  diffiunisros  34569  elcarsg  34695  carsgclctunlem2  34709  carsgclctun  34711  ballotlemfval  34880  ballotlemgval  34914  fineqvomon  35531  cvmscbv  35750  cvmsdisj  35762  cvmsss2  35766  satfv1  35855  nepss  36210  tailfb  36908  dfttc4lem1  37059  bj-0int  37763  mblfinlem2  38329  qsdisjALTV  39368  disjimeceqim  39473  lshpinN  39783  elrfi  43445  fipjust  44311  conrel1d  44409  ntrk0kbimka  44785  clsk3nimkb  44786  isotone2  44795  ntrclskb  44815  ntrclsk3  44816  ntrclsk13  44817  csbresgVD  45623  wfac8prim  45731  permac8prim  45743  disjf1  45921  qinioo  46271  fouriersw  46965  nnfoctbdjlem  47189  meadjun  47196  caragenel  47229  sepnsepolem2  49721  sepfsepc  49726  iscnrm3rlem8  49745  iscnrm3llem2  49748