Theorem ineq2 4167

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913

This theorem is used by:  ineq12  4168  ineq2i  4170  ineq2d  4173  uneqin  4242  wefrc  5657  onfr  6404  onnseq  8337  qsdisj  8798  disjenex  9130  fiint  9293  elfiun  9397  dffi3  9398  cplem2  9888  cplem2OLD  9889  dfac5  10128  kmlem2  10151  kmlem13  10162  kmlem14  10163  ackbij1lem16  10233  fin23lem12  10330  fin23lem19  10335  fin23lem33  10344  uzin2  15422  pgpfac1lem3  20195  pgpfac1lem5  20197  pgpfac1  20198  ssdifidllem  21536  ssdifidl  21537  ssdifidlprm  21538  inopn  23108  basis1  23159  basis2  23160  baspartn  23163  fctop  23213  cctop  23215  ordtbaslem  23397  hausnei2  23562  cnhaus  23563  nrmsep  23566  isnrm2  23567  dishaus  23591  ordthauslem  23592  dfconn2  23628  nconnsubb  23632  finlocfin  23730  dissnlocfin  23739  locfindis  23740  kgeni  23747  pthaus  23848  txhaus  23857  xkohaus  23863  regr1lem  23949  fbasssin  24046  fbun  24050  fbunfip  24079  filconn  24093  isufil2  24118  ufileu  24129  filufint  24130  fmfnfmlem4  24167  fmfnfm  24168  fclsopni  24225  fclsbas  24231  fclsrest  24234  isfcf  24244  tsmsfbas  24338  ustincl  24418  ust0  24430  metreslem  24572  methaus  24730  qtopbaslem  24968  metnrmlem3  25072  ismbl  25738  shincl  31806  chincl  31924  chdmm1  31950  ledi  31965  cmbr  32009  cmbr3i  32025  cmbr3  32033  pjoml2  32036  stcltrlem1  32701  mdbr  32719  dmdbr  32724  cvmd  32761  cvexch  32799  sumdmdii  32840  mddmdin0i  32856  ofpreima2  33084  1arithufdlem4  33903  crefeq  34301  ldgenpisyslem1  34620  ldgenpisys  34623  inelsros  34635  diffiunisros  34636  elcarsg  34762  carsgclctunlem2  34776  carsgclctun  34778  ballotlemfval  34947  ballotlemgval  34981  fineqvomon  35590  cvmscbv  35789  cvmsdisj  35801  cvmsss2  35805  satfv1  35894  nepss  36249  tailfb  36947  dfttc4lem1  37098  bj-0int  37802  mblfinlem2  38368  qsdisjALTV  39408  disjimeceqim  39513  lshpinN  39823  elrfi  43485  fipjust  44351  conrel1d  44449  ntrk0kbimka  44825  clsk3nimkb  44826  isotone2  44835  ntrclskb  44855  ntrclsk3  44856  ntrclsk13  44857  csbresgVD  45663  wfac8prim  45771  permac8prim  45783  disjf1  45961  qinioo  46311  fouriersw  47005  nnfoctbdjlem  47229  meadjun  47236  caragenel  47269  sepnsepolem2  49760  sepfsepc  49765  iscnrm3rlem8  49784  iscnrm3llem2  49787