Theorem un0 3448

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	⊢ (𝐴 ∪ ∅) = 𝐴

Proof of Theorem un0

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3418	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 741	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 131	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 3269	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 703   = wceq 1348   ∈ wcel 2141   ∪ cun 3119  ∅c0 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123  df-un 3125  df-nul 3415

This theorem is referenced by:  un00  3461  disjssun  3478  difun2  3494  difdifdirss  3499  disjpr2  3647  prprc1  3691  diftpsn3  3721  iununir  3956  suc0  4396  sucprc  4397  fvun1  5562  fmptpr  5688  fvunsng  5690  fvsnun1  5693  fvsnun2  5694  fsnunfv  5697  fsnunres  5698  rdg0  6366  omv2  6444  unsnfidcex  6897  unfidisj  6899  undifdc  6901  ssfirab  6911  dju0en  7191  djuassen  7194  fzsuc2  10035  fseq1p1m1  10050  hashunlem  10739  ennnfonelem1  12362  setsresg  12454  setsslid  12466  fmelpw1o  13841  exmid1stab  14033