Theorem ineq2 4175

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

Syntax hints:   → wi 4   = wceq 1567   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920

This theorem is referenced by:  ineq12  4176  ineq2i  4178  ineq2d  4181  uneqin  4250  wefrc  5656  onfr  6401  onnseq  8331  qsdisj  8792  disjenex  9123  fiint  9286  elfiun  9390  dffi3  9391  cplem2  9876  dfac5  10112  kmlem2  10135  kmlem13  10146  kmlem14  10147  ackbij1lem16  10217  fin23lem12  10315  fin23lem19  10320  fin23lem33  10329  uzin2  15396  pgpfac1lem3  20149  pgpfac1lem5  20151  pgpfac1  20152  ssdifidllem  21453  ssdifidl  21454  ssdifidlprm  21455  inopn  23025  basis1  23076  basis2  23077  baspartn  23080  fctop  23130  cctop  23132  ordtbaslem  23314  hausnei2  23479  cnhaus  23480  nrmsep  23483  isnrm2  23484  dishaus  23508  ordthauslem  23509  dfconn2  23545  nconnsubb  23549  finlocfin  23646  dissnlocfin  23655  locfindis  23656  kgeni  23663  pthaus  23764  txhaus  23773  xkohaus  23779  regr1lem  23865  fbasssin  23962  fbun  23966  fbunfip  23995  filconn  24009  isufil2  24034  ufileu  24045  filufint  24046  fmfnfmlem4  24083  fmfnfm  24084  fclsopni  24141  fclsbas  24147  fclsrest  24150  isfcf  24160  tsmsfbas  24254  ustincl  24334  ust0  24346  metreslem  24488  methaus  24646  qtopbaslem  24884  metnrmlem3  24988  ismbl  25654  shincl  31674  chincl  31792  chdmm1  31818  ledi  31833  cmbr  31877  cmbr3i  31893  cmbr3  31901  pjoml2  31904  stcltrlem1  32569  mdbr  32587  dmdbr  32592  cvmd  32629  cvexch  32667  sumdmdii  32708  mddmdin0i  32724  ofpreima2  32952  1arithufdlem4  33782  crefeq  34180  ldgenpisyslem1  34498  ldgenpisys  34501  inelsros  34513  diffiunisros  34514  elcarsg  34640  carsgclctunlem2  34654  carsgclctun  34656  ballotlemfval  34825  ballotlemgval  34859  fineqvomon  35454  cvmscbv  35649  cvmsdisj  35661  cvmsss2  35665  satfv1  35754  nepss  36109  tailfb  36777  dfttc4lem1  36928  bj-0int  37631  mblfinlem2  38197  qsdisjALTV  39238  disjimeceqim  39343  lshpinN  39653  elrfi  43317  fipjust  44183  conrel1d  44281  ntrk0kbimka  44657  clsk3nimkb  44658  isotone2  44667  ntrclskb  44687  ntrclsk3  44688  ntrclsk13  44689  csbresgVD  45495  wfac8prim  45603  permac8prim  45615  disjf1  45793  qinioo  46143  fouriersw  46837  nnfoctbdjlem  47061  meadjun  47068  caragenel  47101  sepnsepolem2  49586  sepfsepc  49591  iscnrm3rlem8  49610  iscnrm3llem2  49613