Theorem ineq2 4114

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094

This theorem is used by:  ineq12  4115  ineq2i  4117  ineq2d  4120  uneqin  4237  wefrc  5652  onfr  6428  onnseq  8390  qsdisj  8853  disjenex  9192  fiint  9356  elfiun  9459  dffi3  9460  cplem2  9989  cplem2OLD  9990  dfac5  10246  kmlem2  10269  kmlem13  10280  kmlem14  10281  ackbij1lem16  10351  fin23lem12  10448  fin23lem19  10453  fin23lem33  10462  uzin2  15556  pgpfac1lem3  20344  pgpfac1lem5  20346  pgpfac1  20347  ssdifidllem  21691  ssdifidl  21692  ssdifidlprm  21693  inopn  23272  basis1  23323  basis2  23324  baspartn  23327  fctop  23377  cctop  23379  ordtbaslem  23561  hausnei2  23726  cnhaus  23727  nrmsep  23730  isnrm2  23731  dishaus  23755  ordthauslem  23756  dfconn2  23792  nconnsubb  23796  finlocfin  23894  dissnlocfin  23903  locfindis  23904  kgeni  23911  pthaus  24012  txhaus  24021  xkohaus  24027  regr1lem  24113  fbasssin  24210  fbun  24214  fbunfip  24243  filconn  24257  isufil2  24282  ufileu  24293  filufint  24294  fmfnfmlem4  24331  fmfnfm  24332  fclsopni  24389  fclsbas  24395  fclsrest  24398  isfcf  24408  tsmsfbas  24502  ustincl  24582  ust0  24594  metreslem  24736  methaus  24894  qtopbaslem  25132  metnrmlem3  25236  ismbl  25902  shincl  32040  chincl  32158  chdmm1  32184  ledi  32199  cmbr  32243  cmbr3i  32259  cmbr3  32267  pjoml2  32270  stcltrlem1  32935  mdbr  32953  dmdbr  32958  cvmd  32995  cvexch  33033  sumdmdii  33074  mddmdin0i  33090  ofpreima2  33358  1arithufdlem4  34183  crefeq  34588  ldgenpisyslem1  34907  ldgenpisys  34910  inelsros  34922  diffiunisros  34923  elcarsg  35048  carsgclctunlem2  35062  carsgclctun  35064  ballotlemfval  35233  ballotlemgval  35267  fineqvomon  35927  cvmscbv  36231  cvmsdisj  36243  cvmsss2  36247  satfv1  36336  mirimanofffr  36670  nepss  36698  tailfb  37380  dfttc4lem1  37531  bj-0int  38292  mblfinlem2  38844  qsdisjALTV  39897  disjimeceqim  40002  lshpinN  40312  elrfi  43971  fipjust  44827  conrel1d  44924  ntrk0kbimka  45300  clsk3nimkb  45301  isotone2  45310  ntrclskb  45330  ntrclsk3  45331  ntrclsk13  45332  csbresgVD  46137  wfac8prim  46256  permac8prim  46268  disjf1  46471  qinioo  46820  fouriersw  47514  nnfoctbdjlem  47738  meadjun  47745  caragenel  47778  sepnsepolem2  50368  sepfsepc  50373  iscnrm3rlem8  50392  iscnrm3llem2  50395