Theorem ineq2 4187

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

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-in 3931

This theorem is referenced by:  ineq12  4188  ineq2i  4190  ineq2d  4193  uneqin  4262  wefrc  5645  onfr  6388  onnseq  8352  qsdisj  8802  disjenex  9143  fiint  9332  fiintOLD  9333  elfiun  9436  dffi3  9437  cplem2  9896  dfac5  10135  kmlem2  10158  kmlem13  10169  kmlem14  10170  ackbij1lem16  10240  fin23lem12  10337  fin23lem19  10342  fin23lem33  10351  uzin2  15350  pgpfac1lem3  20045  pgpfac1lem5  20047  pgpfac1  20048  inopn  22822  basis1  22873  basis2  22874  baspartn  22877  fctop  22927  cctop  22929  ordtbaslem  23111  hausnei2  23276  cnhaus  23277  nrmsep  23280  isnrm2  23281  dishaus  23305  ordthauslem  23306  dfconn2  23342  nconnsubb  23346  finlocfin  23443  dissnlocfin  23452  locfindis  23453  kgeni  23460  pthaus  23561  txhaus  23570  xkohaus  23576  regr1lem  23662  fbasssin  23759  fbun  23763  fbunfip  23792  filconn  23806  isufil2  23831  ufileu  23842  filufint  23843  fmfnfmlem4  23880  fmfnfm  23881  fclsopni  23938  fclsbas  23944  fclsrest  23947  isfcf  23957  tsmsfbas  24051  ustincl  24131  ust0  24143  metreslem  24286  methaus  24444  qtopbaslem  24682  metnrmlem3  24786  ismbl  25464  shincl  31294  chincl  31412  chdmm1  31438  ledi  31453  cmbr  31497  cmbr3i  31513  cmbr3  31521  pjoml2  31524  stcltrlem1  32189  mdbr  32207  dmdbr  32212  cvmd  32249  cvexch  32287  sumdmdii  32328  mddmdin0i  32344  ofpreima2  32577  ssdifidllem  33389  ssdifidl  33390  ssdifidlprm  33391  1arithufdlem4  33480  crefeq  33784  ldgenpisyslem1  34102  ldgenpisys  34105  inelsros  34117  diffiunisros  34118  elcarsg  34245  carsgclctunlem2  34259  carsgclctun  34261  ballotlemfval  34430  ballotlemgval  34464  cvmscbv  35201  cvmsdisj  35213  cvmsss2  35217  satfv1  35306  nepss  35656  tailfb  36316  bj-0int  37040  mblfinlem2  37603  qsdisjALTV  38554  lshpinN  38928  elrfi  42642  fipjust  43514  conrel1d  43612  ntrk0kbimka  43988  clsk3nimkb  43989  isotone2  43998  ntrclskb  44018  ntrclsk3  44019  ntrclsk13  44020  csbresgVD  44846  wfac8prim  44954  disjf1  45134  qinioo  45492  fouriersw  46190  nnfoctbdjlem  46414  meadjun  46421  caragenel  46454  sepnsepolem2  48776  sepfsepc  48781  iscnrm3rlem8  48800  iscnrm3llem2  48803