ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elssuni Structured version   Unicode version

Theorem elssuni 3599
Description: An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
elssuni  C_ 
U.

Proof of Theorem elssuni
StepHypRef Expression
1 ssid 2958 . 2  C_
2 ssuni 3593 . 2  C_  C_  U.
31, 2mpan 400 1  C_ 
U.
Colors of variables: wff set class
Syntax hints:   wi 4   wcel 1390    C_ wss 2911   U.cuni 3571
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-in 2918  df-ss 2925  df-uni 3572
This theorem is referenced by:  unissel  3600  ssunieq  3604  pwuni  3934  pwel  3945  uniopel  3984  iunpw  4177  dmrnssfld  4538  fvssunirng  5133  relfvssunirn  5134  sefvex  5139  riotaexg  5415  pwuninel2  5838  tfrlem9  5876  tfrexlem  5889  unirnioo  8572  bj-elssuniab  9199
  Copyright terms: Public domain W3C validator