Theorem un0 3316

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 u. (/) ) = A

Proof of Theorem un0

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3290	. . . 4 |- -. x e. (/)
2	1	biorfi 700	. . 3 |- ( x e. A <-> ( x e. A \/ x e. (/) ) )
3	2	bicomi 130	. 2 |- ( ( x e. A \/ x e. (/) ) <-> x e. A )
4	3	uneqri 3142	1 |- ( A u. (/) ) = A

Syntax hints:   \/ wo 664   = wceq 1289   e. wcel 1438   u. cun 2997   (/)c0 3286

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-dif 3001  df-un 3003  df-nul 3287

This theorem is referenced by:  un00  3329  disjssun  3346  difun2  3362  difdifdirss  3367  disjpr2  3506  prprc1  3550  diftpsn3  3578  iununir  3812  suc0  4238  sucprc  4239  fvun1  5370  fmptpr  5489  fvunsng  5491  fvsnun1  5494  fvsnun2  5495  fsnunfv  5498  fsnunres  5499  rdg0  6152  omv2  6226  unsnfidcex  6628  unfidisj  6630  undifdc  6632  ssfirab  6641  fzsuc2  9489  fseq1p1m1  9504  hashunlem  10208  setsresg  11527  setsidn  11539