Theorem un0 3496

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

Syntax hints:   ∨ wo 710   = wceq 1373   ∈ wcel 2177   ∪ cun 3166  ∅c0 3462

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-dif 3170  df-un 3172  df-nul 3463

This theorem is referenced by:  un00  3509  disjssun  3526  difun2  3542  difdifdirss  3547  disjpr2  3699  prprc1  3743  diftpsn3  3777  iununir  4014  exmid1stab  4257  suc0  4463  sucprc  4464  fvun1  5655  fmptpr  5786  fvunsng  5788  fvsnun1  5791  fvsnun2  5792  fsnunfv  5795  fsnunres  5796  rdg0  6483  omv2  6561  unsnfidcex  7029  unfidisj  7031  undifdc  7033  ssfirab  7045  dju0en  7339  djuassen  7342  fzsuc2  10214  fseq1p1m1  10229  hashunlem  10962  ennnfonelem1  12828  setsresg  12920  setsslid  12933  lgsquadlem2  15605  fmelpw1o  15856