Theorem ineq2 4193

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3426  df-in 3942

This theorem is referenced by:  ineq12  4194  ineq2i  4196  ineq2d  4199  uneqin  4265  intprgOLD  4972  wefrc  5654  onfr  6383  onnseq  8317  qsdisj  8762  disjenex  9108  fiint  9297  elfiun  9397  dffi3  9398  cplem2  9857  dfac5  10095  kmlem2  10118  kmlem13  10129  kmlem14  10130  ackbij1lem16  10202  fin23lem12  10298  fin23lem19  10303  fin23lem33  10312  uzin2  15263  pgpfac1lem3  19892  pgpfac1lem5  19894  pgpfac1  19895  inopn  22307  basis1  22359  basis2  22360  baspartn  22363  fctop  22413  cctop  22415  ordtbaslem  22598  hausnei2  22763  cnhaus  22764  nrmsep  22767  isnrm2  22768  dishaus  22792  ordthauslem  22793  dfconn2  22829  nconnsubb  22833  finlocfin  22930  dissnlocfin  22939  locfindis  22940  kgeni  22947  pthaus  23048  txhaus  23057  xkohaus  23063  regr1lem  23149  fbasssin  23246  fbun  23250  fbunfip  23279  filconn  23293  isufil2  23318  ufileu  23329  filufint  23330  fmfnfmlem4  23367  fmfnfm  23368  fclsopni  23425  fclsbas  23431  fclsrest  23434  isfcf  23444  tsmsfbas  23538  ustincl  23618  ust0  23630  metreslem  23774  methaus  23935  qtopbaslem  24181  metnrmlem3  24283  ismbl  24949  shincl  30427  chincl  30545  chdmm1  30571  ledi  30586  cmbr  30630  cmbr3i  30646  cmbr3  30654  pjoml2  30657  stcltrlem1  31322  mdbr  31340  dmdbr  31345  cvmd  31382  cvexch  31420  sumdmdii  31461  mddmdin0i  31477  ofpreima2  31690  crefeq  32556  ldgenpisyslem1  32892  ldgenpisys  32895  inelsros  32907  diffiunisros  32908  elcarsg  33035  carsgclctunlem2  33049  carsgclctun  33051  ballotlemfval  33219  ballotlemgval  33253  cvmscbv  33980  cvmsdisj  33992  cvmsss2  33996  satfv1  34085  nepss  34417  tailfb  34966  bj-0int  35686  mblfinlem2  36230  qsdisjALTV  37190  lshpinN  37564  elrfi  41115  fipjust  41999  conrel1d  42097  ntrk0kbimka  42473  clsk3nimkb  42474  isotone2  42483  ntrclskb  42503  ntrclsk3  42504  ntrclsk13  42505  csbresgVD  43339  disjf1  43563  qinioo  43933  fouriersw  44632  nnfoctbdjlem  44856  meadjun  44863  caragenel  44896  sepnsepolem2  47115  sepfsepc  47120  iscnrm3rlem8  47140  iscnrm3llem2  47143