Theorem ineqcomi 4111

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

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-rab 3417  df-in 4094

This theorem is used by:  dfss7  4151  0in  4350  disjdifr  4430  iinrab2  5033  resdmdfsn  6039  imadifssranOLD  6221  cnvimainrn  7098  cnfldfunALT  21745  psdmul  22542  xrlimcnp  27353  nn0diffz0  33482  inv2  35822  vonf1wev  36077  vonf1owevOLD  36079  inres2  39445  ecqmap  39647  readvrec  43679  limsupvaluz  46991  isubgr0uhgr  49244