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

Theorem intssuni 4721
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 4284 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑦𝐴 𝑥𝑦) → ∃𝑦𝐴 𝑥𝑦)
21ex 403 . . 3 (𝐴 ≠ ∅ → (∀𝑦𝐴 𝑥𝑦 → ∃𝑦𝐴 𝑥𝑦))
3 vex 3417 . . . 4 𝑥 ∈ V
43elint2 4706 . . 3 (𝑥 𝐴 ↔ ∀𝑦𝐴 𝑥𝑦)
5 eluni2 4664 . . 3 (𝑥 𝐴 ↔ ∃𝑦𝐴 𝑥𝑦)
62, 4, 53imtr4g 288 . 2 (𝐴 ≠ ∅ → (𝑥 𝐴𝑥 𝐴))
76ssrdv 3833 1 (𝐴 ≠ ∅ → 𝐴 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2164  wne 2999  wral 3117  wrex 3118  wss 3798  c0 4146   cuni 4660   cint 4699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-v 3416  df-dif 3801  df-in 3805  df-ss 3812  df-nul 4147  df-uni 4661  df-int 4700
This theorem is referenced by:  unissint  4723  intssuni2  4724  fin23lem31  9487  wunint  9859  tskint  9929  incexc  14950  incexc2  14951  subgint  17976  efgval  18488  lbsextlem3  19528  cssmre  20407  uffixfr  22104  uffix2  22105  uffixsn  22106  insiga  30741  dfon2lem8  32228  bj-intss  33575  intidl  34369  elrfi  38100
  Copyright terms: Public domain W3C validator