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

Theorem intex 4951
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 4078 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
2 intss1 4626 . . . . 5 (𝑥𝐴 𝐴𝑥)
3 vex 3354 . . . . . 6 𝑥 ∈ V
43ssex 4936 . . . . 5 ( 𝐴𝑥 𝐴 ∈ V)
52, 4syl 17 . . . 4 (𝑥𝐴 𝐴 ∈ V)
65exlimiv 2010 . . 3 (∃𝑥 𝑥𝐴 𝐴 ∈ V)
71, 6sylbi 207 . 2 (𝐴 ≠ ∅ → 𝐴 ∈ V)
8 vprc 4930 . . . 4 ¬ V ∈ V
9 inteq 4614 . . . . . 6 (𝐴 = ∅ → 𝐴 = ∅)
10 int0 4625 . . . . . 6 ∅ = V
119, 10syl6eq 2821 . . . . 5 (𝐴 = ∅ → 𝐴 = V)
1211eleq1d 2835 . . . 4 (𝐴 = ∅ → ( 𝐴 ∈ V ↔ V ∈ V))
138, 12mtbiri 316 . . 3 (𝐴 = ∅ → ¬ 𝐴 ∈ V)
1413necon2ai 2972 . 2 ( 𝐴 ∈ V → 𝐴 ≠ ∅)
157, 14impbii 199 1 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1631  wex 1852  wcel 2145  wne 2943  Vcvv 3351  wss 3723  c0 4063   cint 4611
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737  df-nul 4064  df-int 4612
This theorem is referenced by:  intnex  4952  intexab  4953  iinexg  4955  onint0  7143  onintrab  7148  onmindif2  7159  fival  8474  elfi2  8476  elfir  8477  dffi2  8485  elfiun  8492  fifo  8494  tz9.1c  8770  tz9.12lem1  8814  tz9.12lem3  8816  rankf  8821  cardf2  8969  cardval3  8978  cardid2  8979  cardcf  9276  cflim2  9287  intwun  9759  wuncval  9766  inttsk  9798  intgru  9838  gruina  9842  dfrtrcl2  14010  mremre  16472  mrcval  16478  asplss  19544  aspsubrg  19546  toponmre  21118  subbascn  21279  insiga  30540  sigagenval  30543  sigagensiga  30544  dmsigagen  30547  dfon2lem8  32031  dfon2lem9  32032  bj-snmoore  33400  igenval  34192  pclvalN  35698  elrfi  37783  ismrcd1  37787  mzpval  37821  dmmzp  37822  salgenval  41058  intsal  41065
  Copyright terms: Public domain W3C validator