Theorem uni0 2520

Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 2705 by Eric Schmidt, 4-Apr-2007.)

Assertion

Ref	Expression
uni0	|- U.(/) = (/)

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 2297	. 2 |- (/) (_ {(/)}
2		uni0b 2518	. 2 |- (U.(/) = (/) <-> (/) (_ {(/)})
3	1, 2	mpbir 190	1 |- U.(/) = (/)

Syntax hints:   = wceq 954   (_ wss 2043  (/)c0 2276  {csn 2405  U.cuni 2498

This theorem is referenced by:  unisn2 2870  unizlim 3108  unixp0 3510  fvprc 3712  funfv 3761  fvopabn 3777  1stval 4071  2ndval 4072  1st0 4073  2nd0 4074  1st2val 4085  2nd2val 4086  unifi 4538  infeq5 4601  rankuni 4678  rankxplim3 4694  dffsum 6944  isumnul 7146  0opnt 7551  sn0top 7597  indistop 7598

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-in 2047  df-ss 2049  df-nul 2277  df-sn 2408  df-uni 2499

Copyright terms: Public domain