Theorem un0 3362

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 3333	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 718	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 131	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 3184	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 680   = wceq 1314   ∈ wcel 1463   ∪ cun 3035  ∅c0 3329

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-dif 3039  df-un 3041  df-nul 3330

This theorem is referenced by:  un00  3375  disjssun  3392  difun2  3408  difdifdirss  3413  disjpr2  3553  prprc1  3597  diftpsn3  3627  iununir  3862  suc0  4293  sucprc  4294  fvun1  5441  fmptpr  5566  fvunsng  5568  fvsnun1  5571  fvsnun2  5572  fsnunfv  5575  fsnunres  5576  rdg0  6238  omv2  6315  unsnfidcex  6761  unfidisj  6763  undifdc  6765  ssfirab  6774  dju0en  7018  djuassen  7021  fzsuc2  9752  fseq1p1m1  9767  hashunlem  10443  ennnfonelem1  11765  setsresg  11840  setsslid  11852  exmid1stab  12887