Theorem ineqcomi 4172

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

Syntax hints:   = wceq 1567   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-rab 3424  df-in 3920

This theorem is referenced by:  dfss7  4212  0in  4361  disjdifr  4439  iinrab2  5038  resdmdfsn  6032  imadifssran  6203  cnvimainrn  7063  cnfldfunALT  21506  psdmul  22298  xrlimcnp  27099  nn0diffz0  33080  vonf1wev  35491  vonf1owevOLD  35493  inres2  38786  ecqmap  38988  readvrec  43013  limsupvaluz  46314  isubgr0uhgr  48527