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 2786	1 ⊢ (𝐵 ∩ 𝐴) = 𝐶

Syntax hints:   = wceq 1570   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-rab 3417  df-in 3912

This theorem is referenced by:  dfss7  4204  0in  4354  disjdifr  4434  iinrab2  5034  resdmdfsn  6031  imadifssran  6202  cnvimainrn  7062  cnfldfunALT  21537  psdmul  22329  xrlimcnp  27133  nn0diffz0  33139  inv2  35467  vonf1wev  35592  vonf1owevOLD  35594  inres2  38916  ecqmap  39118  readvrec  43143  limsupvaluz  46442  isubgr0uhgr  48658