Theorem ineq2 4143

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

Syntax hints:   → wi 4   = wceq 1547   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-in 3890

This theorem is referenced by:  ineq12  4144  ineq2i  4146  ineq2d  4149  uneqin  4217  wefrc  5612  onfr  6349  onnseq  8274  qsdisj  8731  disjenex  9063  fiint  9227  elfiun  9333  dffi3  9334  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  22882  basis1  22933  basis2  22934  baspartn  22937  fctop  22987  cctop  22989  ordtbaslem  23171  hausnei2  23336  cnhaus  23337  nrmsep  23340  isnrm2  23341  dishaus  23365  ordthauslem  23366  dfconn2  23402  nconnsubb  23406  finlocfin  23503  dissnlocfin  23512  locfindis  23513  kgeni  23520  pthaus  23621  txhaus  23630  xkohaus  23636  regr1lem  23722  fbasssin  23819  fbun  23823  fbunfip  23852  filconn  23866  isufil2  23891  ufileu  23902  filufint  23903  fmfnfmlem4  23940  fmfnfm  23941  fclsopni  23998  fclsbas  24004  fclsrest  24007  isfcf  24017  tsmsfbas  24111  ustincl  24191  ust0  24203  metreslem  24345  methaus  24503  qtopbaslem  24741  metnrmlem3  24845  ismbl  25511  shincl  31470  chincl  31588  chdmm1  31614  ledi  31629  cmbr  31673  cmbr3i  31689  cmbr3  31697  pjoml2  31700  stcltrlem1  32365  mdbr  32383  dmdbr  32388  cvmd  32425  cvexch  32463  sumdmdii  32504  mddmdin0i  32520  ofpreima2  32758  ssdifidllem  33539  ssdifidl  33540  ssdifidlprm  33541  1arithufdlem4  33630  crefeq  34029  ldgenpisyslem1  34347  ldgenpisys  34350  inelsros  34362  diffiunisros  34363  elcarsg  34489  carsgclctunlem2  34503  carsgclctun  34505  ballotlemfval  34674  ballotlemgval  34708  fineqvomon  35299  cvmscbv  35486  cvmsdisj  35498  cvmsss2  35502  satfv1  35591  nepss  35946  tailfb  36605  dfttc4lem1  36756  bj-0int  37459  mblfinlem2  38025  qsdisjALTV  39066  disjimeceqim  39171  lshpinN  39481  elrfi  43143  fipjust  44009  conrel1d  44107  ntrk0kbimka  44483  clsk3nimkb  44484  isotone2  44493  ntrclskb  44513  ntrclsk3  44514  ntrclsk13  44515  csbresgVD  45338  wfac8prim  45446  permac8prim  45458  disjf1  45630  qinioo  45980  fouriersw  46674  nnfoctbdjlem  46898  meadjun  46905  caragenel  46938  sepnsepolem2  49413  sepfsepc  49418  iscnrm3rlem8  49437  iscnrm3llem2  49440