Theorem ineqcomi 4164

Description: Two ways of expressing that two classes have a given intersection. Inference form of ineqcom 4163. 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 4162	. 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵)
2		ineqcomi.1	. 2 ⊢ (𝐴 ∩ 𝐵) = 𝐶
3	1, 2	eqtri 2788	1 ⊢ (𝐵 ∩ 𝐴) = 𝐶

This proof depends on syntax axioms:   = 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-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-rab 3419  df-in 3913

This theorem is used by:  dfss7  4204  0in  4354  disjdifr  4434  iinrab2  5036  resdmdfsn  6033  imadifssran  6204  cnvimainrn  7066  cnfldfunALT  21589  psdmul  22381  xrlimcnp  27186  nn0diffz0  33211  inv2  35534  vonf1wev  35651  vonf1owevOLD  35653  inres2  38956  ecqmap  39158  readvrec  43183  limsupvaluz  46482  isubgr0uhgr  48698