Theorem ineq2 4221

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

Syntax hints:   → wi 4   = wceq 1536   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969

This theorem is referenced by:  ineq12  4222  ineq2i  4224  ineq2d  4227  uneqin  4294  wefrc  5682  onfr  6424  onnseq  8382  qsdisj  8832  disjenex  9173  fiint  9363  fiintOLD  9364  elfiun  9467  dffi3  9468  cplem2  9927  dfac5  10166  kmlem2  10189  kmlem13  10200  kmlem14  10201  ackbij1lem16  10271  fin23lem12  10368  fin23lem19  10373  fin23lem33  10382  uzin2  15379  pgpfac1lem3  20111  pgpfac1lem5  20113  pgpfac1  20114  inopn  22920  basis1  22972  basis2  22973  baspartn  22976  fctop  23026  cctop  23028  ordtbaslem  23211  hausnei2  23376  cnhaus  23377  nrmsep  23380  isnrm2  23381  dishaus  23405  ordthauslem  23406  dfconn2  23442  nconnsubb  23446  finlocfin  23543  dissnlocfin  23552  locfindis  23553  kgeni  23560  pthaus  23661  txhaus  23670  xkohaus  23676  regr1lem  23762  fbasssin  23859  fbun  23863  fbunfip  23892  filconn  23906  isufil2  23931  ufileu  23942  filufint  23943  fmfnfmlem4  23980  fmfnfm  23981  fclsopni  24038  fclsbas  24044  fclsrest  24047  isfcf  24057  tsmsfbas  24151  ustincl  24231  ust0  24243  metreslem  24387  methaus  24548  qtopbaslem  24794  metnrmlem3  24896  ismbl  25574  shincl  31409  chincl  31527  chdmm1  31553  ledi  31568  cmbr  31612  cmbr3i  31628  cmbr3  31636  pjoml2  31639  stcltrlem1  32304  mdbr  32322  dmdbr  32327  cvmd  32364  cvexch  32402  sumdmdii  32443  mddmdin0i  32459  ofpreima2  32682  ssdifidllem  33463  ssdifidl  33464  ssdifidlprm  33465  1arithufdlem4  33554  crefeq  33805  ldgenpisyslem1  34143  ldgenpisys  34146  inelsros  34158  diffiunisros  34159  elcarsg  34286  carsgclctunlem2  34300  carsgclctun  34302  ballotlemfval  34470  ballotlemgval  34504  cvmscbv  35242  cvmsdisj  35254  cvmsss2  35258  satfv1  35347  nepss  35697  tailfb  36359  bj-0int  37083  mblfinlem2  37644  qsdisjALTV  38596  lshpinN  38970  elrfi  42681  fipjust  43554  conrel1d  43652  ntrk0kbimka  44028  clsk3nimkb  44029  isotone2  44038  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  csbresgVD  44892  disjf1  45125  qinioo  45487  fouriersw  46186  nnfoctbdjlem  46410  meadjun  46417  caragenel  46450  sepnsepolem2  48718  sepfsepc  48723  iscnrm3rlem8  48743  iscnrm3llem2  48746