Theorem ineqcomi 4163

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

Syntax hints:   = wceq 1560   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-rab 3415  df-in 3911

This theorem is referenced by:  dfss7  4203  0in  4351  disjdifr  4427  iinrab2  5027  resdmdfsn  6018  cnvimainrn  7048  cnfldfunALT  21439  psdmul  22231  xrlimcnp  27033  nn0diffz0  32996  vonf1wev  35451  vonf1owevOLD  35453  inres2  38746  ecqmap  38948  readvrec  42971  limsupvaluz  46282  isubgr0uhgr  48495