MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  intssuni Structured version   Visualization version   GIF version

Theorem intssuni 4901
Description: The intersection of a nonempty set is a subclass of its union. (Contributed by NM, 29-Jul-2006.)
Assertion
Ref Expression
intssuni (𝐴 ≠ ∅ → 𝐴 𝐴)

Proof of Theorem intssuni
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r19.2z 4425 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑦𝐴 𝑥𝑦) → ∃𝑦𝐴 𝑥𝑦)
21ex 413 . . 3 (𝐴 ≠ ∅ → (∀𝑦𝐴 𝑥𝑦 → ∃𝑦𝐴 𝑥𝑦))
3 vex 3436 . . . 4 𝑥 ∈ V
43elint2 4886 . . 3 (𝑥 𝐴 ↔ ∀𝑦𝐴 𝑥𝑦)
5 eluni2 4843 . . 3 (𝑥 𝐴 ↔ ∃𝑦𝐴 𝑥𝑦)
62, 4, 53imtr4g 296 . 2 (𝐴 ≠ ∅ → (𝑥 𝐴𝑥 𝐴))
76ssrdv 3927 1 (𝐴 ≠ ∅ → 𝐴 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wne 2943  wral 3064  wrex 3065  wss 3887  c0 4256   cuni 4839   cint 4879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257  df-uni 4840  df-int 4880
This theorem is referenced by:  unissint  4903  intssuni2  4904  intss2  5037  fin23lem31  10099  wunint  10471  tskint  10541  incexc  15549  incexc2  15550  subgint  18779  efgval  19323  lbsextlem3  20422  cssmre  20898  uffixfr  23074  uffix2  23075  uffixsn  23076  ssmxidllem  31641  insiga  32105  dfon2lem8  33766  intidl  36187  elrfi  40516  toplatglb  46287
  Copyright terms: Public domain W3C validator