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

Theorem intssuni 4868
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 4391 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑦𝐴 𝑥𝑦) → ∃𝑦𝐴 𝑥𝑦)
21ex 416 . . 3 (𝐴 ≠ ∅ → (∀𝑦𝐴 𝑥𝑦 → ∃𝑦𝐴 𝑥𝑦))
3 vex 3404 . . . 4 𝑥 ∈ V
43elint2 4853 . . 3 (𝑥 𝐴 ↔ ∀𝑦𝐴 𝑥𝑦)
5 eluni2 4810 . . 3 (𝑥 𝐴 ↔ ∃𝑦𝐴 𝑥𝑦)
62, 4, 53imtr4g 299 . 2 (𝐴 ≠ ∅ → (𝑥 𝐴𝑥 𝐴))
76ssrdv 3893 1 (𝐴 ≠ ∅ → 𝐴 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  wne 2935  wral 3054  wrex 3055  wss 3853  c0 4221   cuni 4806   cint 4846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ne 2936  df-ral 3059  df-rex 3060  df-v 3402  df-dif 3856  df-in 3860  df-ss 3870  df-nul 4222  df-uni 4807  df-int 4847
This theorem is referenced by:  unissint  4870  intssuni2  4871  intss2  5003  fin23lem31  9855  wunint  10227  tskint  10297  incexc  15297  incexc2  15298  subgint  18433  efgval  18973  lbsextlem3  20063  cssmre  20521  uffixfr  22686  uffix2  22687  uffixsn  22688  ssmxidllem  31225  insiga  31687  dfon2lem8  33352  intidl  35842  elrfi  40128
  Copyright terms: Public domain W3C validator