Metamath Proof Explorer

Theorem indm

Description: De Morgan's law for intersection. Theorem 5.2(13') of Stoll p. 19. (Contributed by NM, 18-Aug-2004)

Ref Expression
Assertion indm 
|- ( _V \ ( A i^i B ) ) = ( ( _V \ A ) u. ( _V \ B ) )

Proof

Step Hyp Ref Expression
1 difindi 
 |-  ( _V \ ( A i^i B ) ) = ( ( _V \ A ) u. ( _V \ B ) )