Theorem ineqcomi 4110

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

This proof depends on syntax axioms:   = wceq 1569   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-rab 3416  df-in 4093

This theorem is used by:  dfss7  4150  0in  4349  disjdifr  4429  iinrab2  5030  resdmdfsn  6026  imadifssranOLD  6208  cnvimainrn  7074  cnfldfunALT  21705  psdmul  22499  xrlimcnp  27308  nn0diffz0  33439  inv2  35764  vonf1wev  35990  vonf1owevOLD  35992  inres2  39319  ecqmap  39521  readvrec  43553  limsupvaluz  46857  isubgr0uhgr  49110