Theorem un0 2896

Description: The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27.

Assertion

Ref	Expression
un0	|- (A u. (/)) = A

Proof of Theorem un0

Step	Hyp	Ref	Expression
1		noel 2879	. . . 4 |- -. x e. (/)
2	1	biorfi 808	. . 3 |- (x e. A <-> (x e. A \/ x e. (/)))
3	2	bicomi 189	. 2 |- ((x e. A \/ x e. (/)) <-> x e. A)
4	3	uneqri 2742	1 |- (A u. (/)) = A

Syntax hints:   \/ wo 239   = wceq 1298   e. wcel 1300   u. cun 2591  (/)c0 2875

This theorem is referenced by:  un00 2907  disjssun 2932  difun2 2953  difdifdir 2957  prprc1 3108  unidif0 3476  suc0 3739  sucprc 3740  dfco2aOLD 4395  fvsnun1 4764  fvsnun2 4765  oev2 5207  oarec 5244  mapunen 5596  kmlem2 5928  kmlem3 5929  kmlem11 5937  cda0en 6075  dffsum 8258  dfisum 8452  acdc2lem2 8758  acdc5lem2 8761  ruclem6 8784  alephadd 8851  indistop 8918  indistps 8923  subcld 10254  wfrlem14 13970  axfelem8 14038  axfelem9 14039  repfuntw 14502  unprj 14511  mapudiscn 14872  eqindhome 14895  prtoptop 14919  limfillem2 14939  clindistop 14962  intopcon 14964  topsinind 14967  extopgrp 14980  elfiun 15369  topjoin 15527  filcon 15580  ufcondr 15581  padd01 17272  padd02 17273

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-dif 2597  df-un 2600  df-nul 2876

Copyright terms: Public domain