Theorem ineqcomi 4157

Description: Two ways of expressing that two classes have a given intersection. Inference form of ineqcom 4156. Disjointness inference when 𝐶 = ∅. (Contributed by Peter Mazsa, 26-Mar-2017.) (Proof shortened by SN, 20-Sep-2024.)

Hypothesis

Ref	Expression
ineqcomi.1	⊢ (𝐴 ∩ 𝐵) = 𝐶

Assertion

Ref	Expression
ineqcomi	⊢ (𝐵 ∩ 𝐴) = 𝐶

Proof of Theorem ineqcomi

Step	Hyp	Ref	Expression
1		incom 4155	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		ineqcomi.1	. 2 ⊢ (𝐴 ∩ 𝐵) = 𝐶
3	1, 2	eqtri 2784	1 ⊢ (𝐵 ∩ 𝐴) = 𝐶

This proof depends on syntax axioms:   = 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-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-rab 3414  df-in 3906

This theorem is used by:  dfss7  4197  0in  4347  disjdifr  4427  iinrab2  5028  resdmdfsn  6021  imadifssranOLD  6202  cnvimainrn  7066  cnfldfunALT  21693  psdmul  22487  xrlimcnp  27296  nn0diffz0  33386  inv2  35709  vonf1wev  35887  vonf1owevOLD  35889  inres2  39179  ecqmap  39381  readvrec  43413  limsupvaluz  46717  isubgr0uhgr  48970