Theorem ineq2 4166

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

Syntax hints:   → wi 4   = wceq 1541   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908

This theorem is referenced by:  ineq12  4167  ineq2i  4169  ineq2d  4172  uneqin  4241  wefrc  5618  onfr  6356  onnseq  8276  qsdisj  8731  disjenex  9063  fiint  9227  elfiun  9333  dffi3  9334  cplem2  9802  dfac5  10039  kmlem2  10062  kmlem13  10073  kmlem14  10074  ackbij1lem16  10144  fin23lem12  10241  fin23lem19  10246  fin23lem33  10255  uzin2  15268  pgpfac1lem3  20008  pgpfac1lem5  20010  pgpfac1  20011  inopn  22843  basis1  22894  basis2  22895  baspartn  22898  fctop  22948  cctop  22950  ordtbaslem  23132  hausnei2  23297  cnhaus  23298  nrmsep  23301  isnrm2  23302  dishaus  23326  ordthauslem  23327  dfconn2  23363  nconnsubb  23367  finlocfin  23464  dissnlocfin  23473  locfindis  23474  kgeni  23481  pthaus  23582  txhaus  23591  xkohaus  23597  regr1lem  23683  fbasssin  23780  fbun  23784  fbunfip  23813  filconn  23827  isufil2  23852  ufileu  23863  filufint  23864  fmfnfmlem4  23901  fmfnfm  23902  fclsopni  23959  fclsbas  23965  fclsrest  23968  isfcf  23978  tsmsfbas  24072  ustincl  24152  ust0  24164  metreslem  24306  methaus  24464  qtopbaslem  24702  metnrmlem3  24806  ismbl  25483  shincl  31456  chincl  31574  chdmm1  31600  ledi  31615  cmbr  31659  cmbr3i  31675  cmbr3  31683  pjoml2  31686  stcltrlem1  32351  mdbr  32369  dmdbr  32374  cvmd  32411  cvexch  32449  sumdmdii  32490  mddmdin0i  32506  ofpreima2  32744  ssdifidllem  33537  ssdifidl  33538  ssdifidlprm  33539  1arithufdlem4  33628  crefeq  34002  ldgenpisyslem1  34320  ldgenpisys  34323  inelsros  34335  diffiunisros  34336  elcarsg  34462  carsgclctunlem2  34476  carsgclctun  34478  ballotlemfval  34647  ballotlemgval  34681  fineqvomon  35274  cvmscbv  35452  cvmsdisj  35464  cvmsss2  35468  satfv1  35557  nepss  35912  tailfb  36571  bj-0int  37306  mblfinlem2  37859  qsdisjALTV  38882  lshpinN  39259  elrfi  42946  fipjust  43816  conrel1d  43914  ntrk0kbimka  44290  clsk3nimkb  44291  isotone2  44300  ntrclskb  44320  ntrclsk3  44321  ntrclsk13  44322  csbresgVD  45145  wfac8prim  45253  permac8prim  45265  disjf1  45437  qinioo  45791  fouriersw  46485  nnfoctbdjlem  46709  meadjun  46716  caragenel  46749  sepnsepolem2  49178  sepfsepc  49183  iscnrm3rlem8  49202  iscnrm3llem2  49205