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

Theorem intex 5231
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 4307 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
2 intss1 4882 . . . . 5 (𝑥𝐴 𝐴𝑥)
3 vex 3495 . . . . . 6 𝑥 ∈ V
43ssex 5216 . . . . 5 ( 𝐴𝑥 𝐴 ∈ V)
52, 4syl 17 . . . 4 (𝑥𝐴 𝐴 ∈ V)
65exlimiv 1922 . . 3 (∃𝑥 𝑥𝐴 𝐴 ∈ V)
71, 6sylbi 218 . 2 (𝐴 ≠ ∅ → 𝐴 ∈ V)
8 vprc 5210 . . . 4 ¬ V ∈ V
9 inteq 4870 . . . . . 6 (𝐴 = ∅ → 𝐴 = ∅)
10 int0 4881 . . . . . 6 ∅ = V
119, 10syl6eq 2869 . . . . 5 (𝐴 = ∅ → 𝐴 = V)
1211eleq1d 2894 . . . 4 (𝐴 = ∅ → ( 𝐴 ∈ V ↔ V ∈ V))
138, 12mtbiri 328 . . 3 (𝐴 = ∅ → ¬ 𝐴 ∈ V)
1413necon2ai 3042 . 2 ( 𝐴 ∈ V → 𝐴 ≠ ∅)
157, 14impbii 210 1 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528  wex 1771  wcel 2105  wne 3013  Vcvv 3492  wss 3933  c0 4288   cint 4867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rab 3144  df-v 3494  df-dif 3936  df-in 3940  df-ss 3949  df-nul 4289  df-int 4868
This theorem is referenced by:  intnex  5232  intexab  5233  iinexg  5235  onint0  7500  onintrab  7505  onmindif2  7516  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  9662  cflim2  9673  intwun  10145  wuncval  10152  inttsk  10184  intgru  10224  gruina  10228  dfrtrcl2  14409  mremre  16863  mrcval  16869  asplss  20031  aspsubrg  20033  toponmre  21629  subbascn  21790  insiga  31295  sigagenval  31298  sigagensiga  31299  dmsigagen  31302  dfon2lem8  32932  dfon2lem9  32933  bj-snmoore  34299  igenval  35220  pclvalN  36906  elrfi  39169  ismrcd1  39173  mzpval  39207  dmmzp  39208  salgenval  42483  intsal  42490
  Copyright terms: Public domain W3C validator