Theorem inv2

Description: The intersection of the universal class with a class is itself. A commuted form of inv1 . (Contributed by BTernaryTau, 24-Jun-2026)

	Ref	Expression
Assertion	inv2	⊢ ( V ∩ 𝐴 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		inv1	⊢ ( 𝐴 ∩ V ) = 𝐴
2	1	ineqcomi	⊢ ( V ∩ 𝐴 ) = 𝐴