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

Theorem intex 5344
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 4349 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
2 intss1 4971 . . . . 5 (𝑥𝐴 𝐴𝑥)
3 vex 3466 . . . . . 6 𝑥 ∈ V
43ssex 5326 . . . . 5 ( 𝐴𝑥 𝐴 ∈ V)
52, 4syl 17 . . . 4 (𝑥𝐴 𝐴 ∈ V)
65exlimiv 1926 . . 3 (∃𝑥 𝑥𝐴 𝐴 ∈ V)
71, 6sylbi 216 . 2 (𝐴 ≠ ∅ → 𝐴 ∈ V)
8 vprc 5320 . . . 4 ¬ V ∈ V
9 inteq 4957 . . . . . 6 (𝐴 = ∅ → 𝐴 = ∅)
10 int0 4970 . . . . . 6 ∅ = V
119, 10eqtrdi 2782 . . . . 5 (𝐴 = ∅ → 𝐴 = V)
1211eleq1d 2811 . . . 4 (𝐴 = ∅ → ( 𝐴 ∈ V ↔ V ∈ V))
138, 12mtbiri 326 . . 3 (𝐴 = ∅ → ¬ 𝐴 ∈ V)
1413necon2ai 2960 . 2 ( 𝐴 ∈ V → 𝐴 ≠ ∅)
157, 14impbii 208 1 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1534  wex 1774  wcel 2099  wne 2930  Vcvv 3462  wss 3947  c0 4325   cint 4954
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304
This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4326  df-int 4955
This theorem is referenced by:  intnex  5345  intexab  5346  iinexg  5348  onint0  7800  onintrab  7805  onmindif2  7816  fival  9455  elfi2  9457  elfir  9458  dffi2  9466  elfiun  9473  fifo  9475  tz9.1c  9773  tz9.12lem1  9830  tz9.12lem3  9832  rankf  9837  cardf2  9986  cardval3  9995  cardid2  9996  cardcf  10295  cflim2  10306  intwun  10778  wuncval  10785  inttsk  10817  intgru  10857  gruina  10861  dfrtrcl2  15067  mremre  17617  mrcval  17623  asplss  21871  aspsubrg  21873  toponmre  23088  subbascn  23249  zarclsint  33687  insiga  33970  sigagenval  33973  sigagensiga  33974  dmsigagen  33977  dfon2lem8  35614  dfon2lem9  35615  bj-snmoore  36820  igenval  37762  pclvalN  39589  elrfi  42351  ismrcd1  42355  mzpval  42389  dmmzp  42390  oninfex2  42910  salgenval  45942  intsal  45951
  Copyright terms: Public domain W3C validator