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

Theorem intex 5207
Description: The intersection of a nonempty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.)
Assertion
Ref Expression
intex (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)

Proof of Theorem intex
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 n0 4263 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
2 intss1 4856 . . . . 5 (𝑥𝐴 𝐴𝑥)
3 vex 3447 . . . . . 6 𝑥 ∈ V
43ssex 5192 . . . . 5 ( 𝐴𝑥 𝐴 ∈ V)
52, 4syl 17 . . . 4 (𝑥𝐴 𝐴 ∈ V)
65exlimiv 1931 . . 3 (∃𝑥 𝑥𝐴 𝐴 ∈ V)
71, 6sylbi 220 . 2 (𝐴 ≠ ∅ → 𝐴 ∈ V)
8 vprc 5186 . . . 4 ¬ V ∈ V
9 inteq 4844 . . . . . 6 (𝐴 = ∅ → 𝐴 = ∅)
10 int0 4855 . . . . . 6 ∅ = V
119, 10eqtrdi 2852 . . . . 5 (𝐴 = ∅ → 𝐴 = V)
1211eleq1d 2877 . . . 4 (𝐴 = ∅ → ( 𝐴 ∈ V ↔ V ∈ V))
138, 12mtbiri 330 . . 3 (𝐴 = ∅ → ¬ 𝐴 ∈ V)
1413necon2ai 3019 . 2 ( 𝐴 ∈ V → 𝐴 ≠ ∅)
157, 14impbii 212 1 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wex 1781  wcel 2112  wne 2990  Vcvv 3444  wss 3884  c0 4246   cint 4841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-sep 5170
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-ral 3114  df-rab 3118  df-v 3446  df-dif 3887  df-in 3891  df-ss 3901  df-nul 4247  df-int 4842
This theorem is referenced by:  intnex  5208  intexab  5209  iinexg  5211  onint0  7495  onintrab  7500  onmindif2  7511  fival  8864  elfi2  8866  elfir  8867  dffi2  8875  elfiun  8882  fifo  8884  tz9.1c  9160  tz9.12lem1  9204  tz9.12lem3  9206  rankf  9211  cardf2  9360  cardval3  9369  cardid2  9370  cardcf  9667  cflim2  9678  intwun  10150  wuncval  10157  inttsk  10189  intgru  10229  gruina  10233  dfrtrcl2  14417  mremre  16871  mrcval  16877  asplss  20564  aspsubrg  20566  toponmre  21702  subbascn  21863  zarclsint  31229  insiga  31510  sigagenval  31513  sigagensiga  31514  dmsigagen  31517  dfon2lem8  33149  dfon2lem9  33150  bj-snmoore  34529  igenval  35498  pclvalN  37185  elrfi  39632  ismrcd1  39636  mzpval  39670  dmmzp  39671  salgenval  42960  intsal  42967
  Copyright terms: Public domain W3C validator