Theorem ineq2 3841

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

Syntax hints:   → wi 4   = wceq 1523   ∩ cin 3606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614

This theorem is referenced by:  ineq12  3842  ineq2i  3844  ineq2d  3847  uneqin  3911  intprg  4543  wefrc  5137  onfr  5801  onnseq  7486  qsdisj  7867  disjenex  8159  fiint  8278  elfiun  8377  dffi3  8378  cplem2  8791  dfac5  8989  kmlem2  9011  kmlem13  9022  kmlem14  9023  ackbij1lem16  9095  fin23lem12  9191  fin23lem19  9196  fin23lem33  9205  uzin2  14128  pgpfac1lem3  18522  pgpfac1lem5  18524  pgpfac1  18525  inopn  20752  basis1  20802  basis2  20803  baspartn  20806  fctop  20856  cctop  20858  ordtbaslem  21040  hausnei2  21205  cnhaus  21206  nrmsep  21209  isnrm2  21210  dishaus  21234  ordthauslem  21235  dfconn2  21270  nconnsubb  21274  finlocfin  21371  dissnlocfin  21380  locfindis  21381  kgeni  21388  pthaus  21489  txhaus  21498  xkohaus  21504  regr1lem  21590  fbasssin  21687  fbun  21691  fbunfip  21720  filconn  21734  isufil2  21759  ufileu  21770  filufint  21771  fmfnfmlem4  21808  fmfnfm  21809  fclsopni  21866  fclsbas  21872  fclsrest  21875  isfcf  21885  tsmsfbas  21978  ustincl  22058  ust0  22070  metreslem  22214  methaus  22372  qtopbaslem  22609  metnrmlem3  22711  ismbl  23340  shincl  28368  chincl  28486  chdmm1  28512  ledi  28527  cmbr  28571  cmbr3i  28587  cmbr3  28595  pjoml2  28598  stcltrlem1  29263  mdbr  29281  dmdbr  29286  cvmd  29323  cvexch  29361  sumdmdii  29402  mddmdin0i  29418  ofpreima2  29594  crefeq  30040  ldgenpisyslem1  30354  ldgenpisys  30357  inelsros  30369  diffiunisros  30370  elcarsg  30495  carsgclctunlem2  30509  carsgclctun  30511  ballotlemfval  30679  ballotlemgval  30713  cvmscbv  31366  cvmsdisj  31378  cvmsss2  31382  nepss  31725  tailfb  32497  bj-0int  33180  mblfinlem2  33577  lshpinN  34594  elrfi  37574  fipjust  38187  conrel1d  38272  ntrk0kbimka  38654  clsk3nimkb  38655  isotone2  38664  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  csbresgVD  39445  disjf1  39683  qinioo  40080  fouriersw  40766  nnfoctbdjlem  40990  meadjun  40997  caragenel  41030