Theorem ineq2 4113

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-in 4093

This theorem is used by:  ineq12  4114  ineq2i  4116  ineq2d  4119  uneqin  4236  wefrc  5648  onfr  6408  onnseq  8363  qsdisj  8826  disjenex  9165  fiint  9329  elfiun  9432  dffi3  9433  cplem2  9962  cplem2OLD  9963  dfac5  10217  kmlem2  10240  kmlem13  10251  kmlem14  10252  ackbij1lem16  10322  fin23lem12  10419  fin23lem19  10424  fin23lem33  10433  uzin2  15524  pgpfac1lem3  20305  pgpfac1lem5  20307  pgpfac1  20308  ssdifidllem  21652  ssdifidl  21653  ssdifidlprm  21654  inopn  23229  basis1  23280  basis2  23281  baspartn  23284  fctop  23334  cctop  23336  ordtbaslem  23518  hausnei2  23683  cnhaus  23684  nrmsep  23687  isnrm2  23688  dishaus  23712  ordthauslem  23713  dfconn2  23749  nconnsubb  23753  finlocfin  23851  dissnlocfin  23860  locfindis  23861  kgeni  23868  pthaus  23969  txhaus  23978  xkohaus  23984  regr1lem  24070  fbasssin  24167  fbun  24171  fbunfip  24200  filconn  24214  isufil2  24239  ufileu  24250  filufint  24251  fmfnfmlem4  24288  fmfnfm  24289  fclsopni  24346  fclsbas  24352  fclsrest  24355  isfcf  24365  tsmsfbas  24459  ustincl  24539  ust0  24551  metreslem  24693  methaus  24851  qtopbaslem  25089  metnrmlem3  25193  ismbl  25859  shincl  31995  chincl  32113  chdmm1  32139  ledi  32154  cmbr  32198  cmbr3i  32214  cmbr3  32222  pjoml2  32225  stcltrlem1  32890  mdbr  32908  dmdbr  32913  cvmd  32950  cvexch  32988  sumdmdii  33029  mddmdin0i  33045  ofpreima2  33314  1arithufdlem4  34132  crefeq  34530  ldgenpisyslem1  34849  ldgenpisys  34852  inelsros  34864  diffiunisros  34865  elcarsg  34990  carsgclctunlem2  35004  carsgclctun  35006  ballotlemfval  35175  ballotlemgval  35209  fineqvomon  35857  cvmscbv  36144  cvmsdisj  36156  cvmsss2  36160  satfv1  36249  nepss  36610  tailfb  37292  dfttc4lem1  37443  bj-0int  38161  mblfinlem2  38716  qsdisjALTV  39771  disjimeceqim  39876  lshpinN  40186  elrfi  43845  fipjust  44706  conrel1d  44803  ntrk0kbimka  45179  clsk3nimkb  45180  isotone2  45189  ntrclskb  45209  ntrclsk3  45210  ntrclsk13  45211  csbresgVD  46016  wfac8prim  46131  permac8prim  46143  disjf1  46337  qinioo  46686  fouriersw  47380  nnfoctbdjlem  47604  meadjun  47611  caragenel  47644  sepnsepolem2  50176  sepfsepc  50181  iscnrm3rlem8  50200  iscnrm3llem2  50203