Theorem ineq2 4214

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958

This theorem is referenced by:  ineq12  4215  ineq2i  4217  ineq2d  4220  uneqin  4289  wefrc  5679  onfr  6423  onnseq  8384  qsdisj  8834  disjenex  9175  fiint  9366  fiintOLD  9367  elfiun  9470  dffi3  9471  cplem2  9930  dfac5  10169  kmlem2  10192  kmlem13  10203  kmlem14  10204  ackbij1lem16  10274  fin23lem12  10371  fin23lem19  10376  fin23lem33  10385  uzin2  15383  pgpfac1lem3  20097  pgpfac1lem5  20099  pgpfac1  20100  inopn  22905  basis1  22957  basis2  22958  baspartn  22961  fctop  23011  cctop  23013  ordtbaslem  23196  hausnei2  23361  cnhaus  23362  nrmsep  23365  isnrm2  23366  dishaus  23390  ordthauslem  23391  dfconn2  23427  nconnsubb  23431  finlocfin  23528  dissnlocfin  23537  locfindis  23538  kgeni  23545  pthaus  23646  txhaus  23655  xkohaus  23661  regr1lem  23747  fbasssin  23844  fbun  23848  fbunfip  23877  filconn  23891  isufil2  23916  ufileu  23927  filufint  23928  fmfnfmlem4  23965  fmfnfm  23966  fclsopni  24023  fclsbas  24029  fclsrest  24032  isfcf  24042  tsmsfbas  24136  ustincl  24216  ust0  24228  metreslem  24372  methaus  24533  qtopbaslem  24779  metnrmlem3  24883  ismbl  25561  shincl  31400  chincl  31518  chdmm1  31544  ledi  31559  cmbr  31603  cmbr3i  31619  cmbr3  31627  pjoml2  31630  stcltrlem1  32295  mdbr  32313  dmdbr  32318  cvmd  32355  cvexch  32393  sumdmdii  32434  mddmdin0i  32450  ofpreima2  32676  ssdifidllem  33484  ssdifidl  33485  ssdifidlprm  33486  1arithufdlem4  33575  crefeq  33844  ldgenpisyslem1  34164  ldgenpisys  34167  inelsros  34179  diffiunisros  34180  elcarsg  34307  carsgclctunlem2  34321  carsgclctun  34323  ballotlemfval  34492  ballotlemgval  34526  cvmscbv  35263  cvmsdisj  35275  cvmsss2  35279  satfv1  35368  nepss  35718  tailfb  36378  bj-0int  37102  mblfinlem2  37665  qsdisjALTV  38616  lshpinN  38990  elrfi  42705  fipjust  43578  conrel1d  43676  ntrk0kbimka  44052  clsk3nimkb  44053  isotone2  44062  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  csbresgVD  44915  wfac8prim  45019  disjf1  45188  qinioo  45548  fouriersw  46246  nnfoctbdjlem  46470  meadjun  46477  caragenel  46510  sepnsepolem2  48820  sepfsepc  48825  iscnrm3rlem8  48844  iscnrm3llem2  48847