Theorem ineq2 4160

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906

This theorem is used by:  ineq12  4161  ineq2i  4163  ineq2d  4166  uneqin  4235  wefrc  5649  onfr  6397  onnseq  8334  qsdisj  8795  disjenex  9134  fiint  9297  elfiun  9401  dffi3  9402  cplem2  9892  cplem2OLD  9893  dfac5  10132  kmlem2  10155  kmlem13  10166  kmlem14  10167  ackbij1lem16  10237  fin23lem12  10334  fin23lem19  10339  fin23lem33  10348  uzin2  15433  pgpfac1lem3  20207  pgpfac1lem5  20209  pgpfac1  20210  ssdifidllem  21548  ssdifidl  21549  ssdifidlprm  21550  inopn  23125  basis1  23176  basis2  23177  baspartn  23180  fctop  23230  cctop  23232  ordtbaslem  23414  hausnei2  23579  cnhaus  23580  nrmsep  23583  isnrm2  23584  dishaus  23608  ordthauslem  23609  dfconn2  23645  nconnsubb  23649  finlocfin  23747  dissnlocfin  23756  locfindis  23757  kgeni  23764  pthaus  23865  txhaus  23874  xkohaus  23880  regr1lem  23966  fbasssin  24063  fbun  24067  fbunfip  24096  filconn  24110  isufil2  24135  ufileu  24146  filufint  24147  fmfnfmlem4  24184  fmfnfm  24185  fclsopni  24242  fclsbas  24248  fclsrest  24251  isfcf  24261  tsmsfbas  24355  ustincl  24435  ust0  24447  metreslem  24589  methaus  24747  qtopbaslem  24985  metnrmlem3  25089  ismbl  25755  shincl  31863  chincl  31981  chdmm1  32007  ledi  32022  cmbr  32066  cmbr3i  32082  cmbr3  32090  pjoml2  32093  stcltrlem1  32758  mdbr  32776  dmdbr  32781  cvmd  32818  cvexch  32856  sumdmdii  32897  mddmdin0i  32913  ofpreima2  33140  1arithufdlem4  33958  crefeq  34356  ldgenpisyslem1  34675  ldgenpisys  34678  inelsros  34690  diffiunisros  34691  elcarsg  34817  carsgclctunlem2  34831  carsgclctun  34833  ballotlemfval  35002  ballotlemgval  35036  fineqvomon  35645  cvmscbv  35838  cvmsdisj  35850  cvmsss2  35854  satfv1  35943  nepss  36298  tailfb  36997  dfttc4lem1  37148  bj-0int  37852  mblfinlem2  38408  qsdisjALTV  39448  disjimeceqim  39553  lshpinN  39863  elrfi  43540  fipjust  44406  conrel1d  44504  ntrk0kbimka  44880  clsk3nimkb  44881  isotone2  44890  ntrclskb  44910  ntrclsk3  44911  ntrclsk13  44912  csbresgVD  45718  wfac8prim  45826  permac8prim  45838  disjf1  46016  qinioo  46366  fouriersw  47060  nnfoctbdjlem  47284  meadjun  47291  caragenel  47324  sepnsepolem2  49850  sepfsepc  49855  iscnrm3rlem8  49874  iscnrm3llem2  49877