Theorem un0 3541

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 3511	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 754	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 132	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 3360	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 716   = wceq 1398   ∈ wcel 2203   ∪ cun 3208  ∅c0 3507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-dif 3212  df-un 3214  df-nul 3508

This theorem is referenced by:  un00  3554  disjssun  3571  difun2  3588  difdifdirss  3593  if0ab  3622  disjpr2  3752  prprc1  3799  diftpsn3  3834  iununir  4074  exmid1stab  4320  suc0  4531  sucprc  4532  fresaunres2disj  5544  fvun1  5742  fmptpr  5875  fvunsng  5877  fvsnun1  5880  fvsnun2  5881  fsnunfv  5884  fsnunres  5885  rdg0  6617  omv2  6697  unsnfidcex  7179  unfidisj  7181  undifdc  7183  ssfirab  7196  dju0en  7520  djuassen  7523  fzsuc2  10412  fseq1p1m1  10427  hashunlem  11166  ennnfonelem1  13150  setsresg  13242  setsslid  13255  lgsquadlem2  15943  gfsump1  16859