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

Theorem intex 4978
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 4095 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
2 intss1 4648 . . . . 5 (𝑥𝐴 𝐴𝑥)
3 vex 3353 . . . . . 6 𝑥 ∈ V
43ssex 4963 . . . . 5 ( 𝐴𝑥 𝐴 ∈ V)
52, 4syl 17 . . . 4 (𝑥𝐴 𝐴 ∈ V)
65exlimiv 2025 . . 3 (∃𝑥 𝑥𝐴 𝐴 ∈ V)
71, 6sylbi 208 . 2 (𝐴 ≠ ∅ → 𝐴 ∈ V)
8 vprc 4958 . . . 4 ¬ V ∈ V
9 inteq 4636 . . . . . 6 (𝐴 = ∅ → 𝐴 = ∅)
10 int0 4647 . . . . . 6 ∅ = V
119, 10syl6eq 2815 . . . . 5 (𝐴 = ∅ → 𝐴 = V)
1211eleq1d 2829 . . . 4 (𝐴 = ∅ → ( 𝐴 ∈ V ↔ V ∈ V))
138, 12mtbiri 318 . . 3 (𝐴 = ∅ → ¬ 𝐴 ∈ V)
1413necon2ai 2966 . 2 ( 𝐴 ∈ V → 𝐴 ≠ ∅)
157, 14impbii 200 1 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652  wex 1874  wcel 2155  wne 2937  Vcvv 3350  wss 3732  c0 4079   cint 4633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-v 3352  df-dif 3735  df-in 3739  df-ss 3746  df-nul 4080  df-int 4634
This theorem is referenced by:  intnex  4979  intexab  4980  iinexg  4982  onint0  7194  onintrab  7199  onmindif2  7210  fival  8525  elfi2  8527  elfir  8528  dffi2  8536  elfiun  8543  fifo  8545  tz9.1c  8821  tz9.12lem1  8865  tz9.12lem3  8867  rankf  8872  cardf2  9020  cardval3  9029  cardid2  9030  cardcf  9327  cflim2  9338  intwun  9810  wuncval  9817  inttsk  9849  intgru  9889  gruina  9893  dfrtrcl2  14089  mremre  16532  mrcval  16538  asplss  19603  aspsubrg  19605  toponmre  21177  subbascn  21338  insiga  30582  sigagenval  30585  sigagensiga  30586  dmsigagen  30589  dfon2lem8  32070  dfon2lem9  32071  bj-snmoore  33428  igenval  34214  pclvalN  35778  elrfi  37867  ismrcd1  37871  mzpval  37905  dmmzp  37906  salgenval  41110  intsal  41117
  Copyright terms: Public domain W3C validator