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 2783	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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-rab 3413  df-in 3906

This theorem is used by:  dfss7  4197  0in  4347  disjdifr  4427  iinrab2  5028  resdmdfsn  6025  imadifssran  6197  cnvimainrn  7060  cnfldfunALT  21603  psdmul  22397  xrlimcnp  27208  nn0diffz0  33268  inv2  35591  vonf1wev  35708  vonf1owevOLD  35710  inres2  38998  ecqmap  39200  readvrec  43240  limsupvaluz  46539  isubgr0uhgr  48792