Theorem ineq2 4164

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

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-in 3906

This theorem is referenced by:  ineq12  4165  ineq2i  4167  ineq2d  4170  uneqin  4239  wefrc  5616  onfr  6354  onnseq  8274  qsdisj  8729  disjenex  9061  fiint  9225  elfiun  9331  dffi3  9332  cplem2  9800  dfac5  10037  kmlem2  10060  kmlem13  10071  kmlem14  10072  ackbij1lem16  10142  fin23lem12  10239  fin23lem19  10244  fin23lem33  10253  uzin2  15266  pgpfac1lem3  20006  pgpfac1lem5  20008  pgpfac1  20009  inopn  22841  basis1  22892  basis2  22893  baspartn  22896  fctop  22946  cctop  22948  ordtbaslem  23130  hausnei2  23295  cnhaus  23296  nrmsep  23299  isnrm2  23300  dishaus  23324  ordthauslem  23325  dfconn2  23361  nconnsubb  23365  finlocfin  23462  dissnlocfin  23471  locfindis  23472  kgeni  23479  pthaus  23580  txhaus  23589  xkohaus  23595  regr1lem  23681  fbasssin  23778  fbun  23782  fbunfip  23811  filconn  23825  isufil2  23850  ufileu  23861  filufint  23862  fmfnfmlem4  23899  fmfnfm  23900  fclsopni  23957  fclsbas  23963  fclsrest  23966  isfcf  23976  tsmsfbas  24070  ustincl  24150  ust0  24162  metreslem  24304  methaus  24462  qtopbaslem  24700  metnrmlem3  24804  ismbl  25481  shincl  31405  chincl  31523  chdmm1  31549  ledi  31564  cmbr  31608  cmbr3i  31624  cmbr3  31632  pjoml2  31635  stcltrlem1  32300  mdbr  32318  dmdbr  32323  cvmd  32360  cvexch  32398  sumdmdii  32439  mddmdin0i  32455  ofpreima2  32693  ssdifidllem  33486  ssdifidl  33487  ssdifidlprm  33488  1arithufdlem4  33577  crefeq  33951  ldgenpisyslem1  34269  ldgenpisys  34272  inelsros  34284  diffiunisros  34285  elcarsg  34411  carsgclctunlem2  34425  carsgclctun  34427  ballotlemfval  34596  ballotlemgval  34630  fineqvomon  35223  cvmscbv  35401  cvmsdisj  35413  cvmsss2  35417  satfv1  35506  nepss  35861  tailfb  36520  bj-0int  37245  mblfinlem2  37798  qsdisjALTV  38811  lshpinN  39188  elrfi  42878  fipjust  43748  conrel1d  43846  ntrk0kbimka  44222  clsk3nimkb  44223  isotone2  44232  ntrclskb  44252  ntrclsk3  44253  ntrclsk13  44254  csbresgVD  45077  wfac8prim  45185  permac8prim  45197  disjf1  45369  qinioo  45723  fouriersw  46417  nnfoctbdjlem  46641  meadjun  46648  caragenel  46681  sepnsepolem2  49110  sepfsepc  49115  iscnrm3rlem8  49134  iscnrm3llem2  49137