Metamath Proof Explorer

Theorem un0

Description: The union of a class with the empty set is itself. Theorem 24 of Suppes p. 27. (Contributed by NM, 15-Jul-1993)

Ref Expression
Assertion un0 A = A


Step Hyp Ref Expression
1 noel ¬ x
2 1 biorfi x A x A x
3 2 bicomi x A x x A
4 3 uneqri A = A