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 4353 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
2 intss1 4963 . . . . 5 (𝑥𝐴 𝐴𝑥)
3 vex 3484 . . . . . 6 𝑥 ∈ V
43ssex 5321 . . . . 5 ( 𝐴𝑥 𝐴 ∈ V)
52, 4syl 17 . . . 4 (𝑥𝐴 𝐴 ∈ V)
65exlimiv 1930 . . 3 (∃𝑥 𝑥𝐴 𝐴 ∈ V)
71, 6sylbi 217 . 2 (𝐴 ≠ ∅ → 𝐴 ∈ V)
8 vprc 5315 . . . 4 ¬ V ∈ V
9 inteq 4949 . . . . . 6 (𝐴 = ∅ → 𝐴 = ∅)
10 int0 4962 . . . . . 6 ∅ = V
119, 10eqtrdi 2793 . . . . 5 (𝐴 = ∅ → 𝐴 = V)
1211eleq1d 2826 . . . 4 (𝐴 = ∅ → ( 𝐴 ∈ V ↔ V ∈ V))
138, 12mtbiri 327 . . 3 (𝐴 = ∅ → ¬ 𝐴 ∈ V)
1413necon2ai 2970 . 2 ( 𝐴 ∈ V → 𝐴 ≠ ∅)
157, 14impbii 209 1 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  wex 1779  wcel 2108  wne 2940  Vcvv 3480  wss 3951  c0 4333   cint 4946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968  df-nul 4334  df-int 4947
This theorem is referenced by:  intnex  5345  intexab  5346  iinexg  5348  onint0  7811  onintrab  7816  onmindif2  7827  fival  9452  elfi2  9454  elfir  9455  dffi2  9463  elfiun  9470  fifo  9472  tz9.1c  9770  tz9.12lem1  9827  tz9.12lem3  9829  rankf  9834  cardf2  9983  cardval3  9992  cardid2  9993  cardcf  10292  cflim2  10303  intwun  10775  wuncval  10782  inttsk  10814  intgru  10854  gruina  10858  dfrtrcl2  15101  mremre  17647  mrcval  17653  asplss  21894  aspsubrg  21896  toponmre  23101  subbascn  23262  zarclsint  33871  insiga  34138  sigagenval  34141  sigagensiga  34142  dmsigagen  34145  dfon2lem8  35791  dfon2lem9  35792  bj-snmoore  37114  igenval  38068  pclvalN  39892  elrfi  42705  ismrcd1  42709  mzpval  42743  dmmzp  42744  oninfex2  43257  salgenval  46336  intsal  46345
  Copyright terms: Public domain W3C validator