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

Theorem intssuni 4469
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 4037 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑦𝐴 𝑥𝑦) → ∃𝑦𝐴 𝑥𝑦)
21ex 450 . . 3 (𝐴 ≠ ∅ → (∀𝑦𝐴 𝑥𝑦 → ∃𝑦𝐴 𝑥𝑦))
3 vex 3192 . . . 4 𝑥 ∈ V
43elint2 4452 . . 3 (𝑥 𝐴 ↔ ∀𝑦𝐴 𝑥𝑦)
5 eluni2 4411 . . 3 (𝑥 𝐴 ↔ ∃𝑦𝐴 𝑥𝑦)
62, 4, 53imtr4g 285 . 2 (𝐴 ≠ ∅ → (𝑥 𝐴𝑥 𝐴))
76ssrdv 3593 1 (𝐴 ≠ ∅ → 𝐴 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wne 2790  wral 2907  wrex 2908  wss 3559  c0 3896   cuni 4407   cint 4445
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-v 3191  df-dif 3562  df-in 3566  df-ss 3573  df-nul 3897  df-uni 4408  df-int 4446
This theorem is referenced by:  unissint  4471  intssuni2  4472  fin23lem31  9117  wunint  9489  tskint  9559  incexc  14505  incexc2  14506  subgint  17550  efgval  18062  lbsextlem3  19092  cssmre  19969  uffixfr  21650  uffix2  21651  uffixsn  21652  insiga  30005  dfon2lem8  31431  intidl  33495  elrfi  36772
  Copyright terms: Public domain W3C validator