Metamath Proof Explorer

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 i^i A ) = A

Proof

Step Hyp Ref Expression
1 inv1 
 |-  ( A i^i _V ) = A
2 1 ineqcomi 
 |-  ( _V i^i A ) = A