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

Theorem intssuni 4970
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 4495 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑦𝐴 𝑥𝑦) → ∃𝑦𝐴 𝑥𝑦)
21ex 412 . . 3 (𝐴 ≠ ∅ → (∀𝑦𝐴 𝑥𝑦 → ∃𝑦𝐴 𝑥𝑦))
3 vex 3484 . . . 4 𝑥 ∈ V
43elint2 4953 . . 3 (𝑥 𝐴 ↔ ∀𝑦𝐴 𝑥𝑦)
5 eluni2 4911 . . 3 (𝑥 𝐴 ↔ ∃𝑦𝐴 𝑥𝑦)
62, 4, 53imtr4g 296 . 2 (𝐴 ≠ ∅ → (𝑥 𝐴𝑥 𝐴))
76ssrdv 3989 1 (𝐴 ≠ ∅ → 𝐴 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  wne 2940  wral 3061  wrex 3070  wss 3951  c0 4333   cuni 4907   cint 4946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-v 3482  df-dif 3954  df-ss 3968  df-nul 4334  df-uni 4908  df-int 4947
This theorem is referenced by:  unissint  4972  intssuni2  4973  intss2  5108  fin23lem31  10383  wunint  10755  tskint  10825  incexc  15873  incexc2  15874  subgint  19168  efgval  19735  lbsextlem3  21162  cssmre  21711  uffixfr  23931  uffix2  23932  uffixsn  23933  ssdifidllem  33484  ssmxidllem  33501  insiga  34138  dfon2lem8  35791  intidl  38036  elrfi  42705  toplatglb  48890
  Copyright terms: Public domain W3C validator