ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  un0 Structured version   GIF version

Theorem un0 3220
Description: The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
un0 (A ∪ ∅) = A

Proof of Theorem un0
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 noel 3197 . . . 4 ¬ x
21biorfi 649 . . 3 (x A ↔ (x A x ∅))
32bicomi 123 . 2 ((x A x ∅) ↔ x A)
43uneqri 3054 1 (A ∪ ∅) = A
Colors of variables: wff set class
Syntax hints:   wo 613   = wceq 1224   wcel 1367  cun 2884  c0 3193
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1310  ax-7 1311  ax-gen 1312  ax-ie1 1356  ax-ie2 1357  ax-8 1369  ax-10 1370  ax-11 1371  ax-i12 1372  ax-bnd 1373  ax-4 1374  ax-17 1393  ax-i9 1397  ax-ial 1401  ax-i5r 1402  ax-ext 1996
This theorem depends on definitions:  df-bi 110  df-tru 1227  df-nf 1324  df-sb 1620  df-clab 2001  df-cleq 2007  df-clel 2010  df-nfc 2141  df-v 2529  df-dif 2889  df-un 2891  df-nul 3194
This theorem is referenced by:  un00  3232  disjssun  3254  difun2  3271  difdifdirss  3276  disjpr2  3398  prprc1  3442  diftpsn3  3469  iununir  3702  suc0  4087  sucprc  4088  fvun1  5153  fmptpr  5269  fvunsng  5271  fvsnun1  5274  fvsnun2  5275  fsnunfv  5277  fsnunres  5278  rdgi0g  5875  rdg0  5884  omv2  5949
  Copyright terms: Public domain W3C validator