Metamath Proof Explorer

Theorem undm

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

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

Proof

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