Theorem un0 3526

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

Syntax hints:   ∨ wo 713   = wceq 1395   ∈ wcel 2200   ∪ cun 3196  ∅c0 3492

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-dif 3200  df-un 3202  df-nul 3493

This theorem is referenced by:  un00  3539  disjssun  3556  difun2  3572  difdifdirss  3577  disjpr2  3731  prprc1  3778  diftpsn3  3812  iununir  4052  exmid1stab  4296  suc0  4506  sucprc  4507  fvun1  5708  fmptpr  5841  fvunsng  5843  fvsnun1  5846  fvsnun2  5847  fsnunfv  5850  fsnunres  5851  rdg0  6548  omv2  6628  unsnfidcex  7107  unfidisj  7109  undifdc  7111  ssfirab  7123  dju0en  7422  djuassen  7425  fmelpw1o  7458  fzsuc2  10307  fseq1p1m1  10322  hashunlem  11060  ennnfonelem1  13021  setsresg  13113  setsslid  13126  lgsquadlem2  15800