**Description:** Idempotent law for union of classes. Theorem 23 of Suppes p. 27.
(Contributed by NM, 21-Jun-1993)

Ref | Expression | ||
---|---|---|---|

Assertion | unidm | $${\u22a2}{A}\cup {A}={A}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | oridm | $${\u22a2}\left({x}\in {A}\vee {x}\in {A}\right)\leftrightarrow {x}\in {A}$$ | |

2 | 1 | uneqri | $${\u22a2}{A}\cup {A}={A}$$ |