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

Theorem intex 5097
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 4198 . . 3 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
2 intss1 4765 . . . . 5 (𝑥𝐴 𝐴𝑥)
3 vex 3418 . . . . . 6 𝑥 ∈ V
43ssex 5082 . . . . 5 ( 𝐴𝑥 𝐴 ∈ V)
52, 4syl 17 . . . 4 (𝑥𝐴 𝐴 ∈ V)
65exlimiv 1889 . . 3 (∃𝑥 𝑥𝐴 𝐴 ∈ V)
71, 6sylbi 209 . 2 (𝐴 ≠ ∅ → 𝐴 ∈ V)
8 vprc 5077 . . . 4 ¬ V ∈ V
9 inteq 4753 . . . . . 6 (𝐴 = ∅ → 𝐴 = ∅)
10 int0 4764 . . . . . 6 ∅ = V
119, 10syl6eq 2830 . . . . 5 (𝐴 = ∅ → 𝐴 = V)
1211eleq1d 2850 . . . 4 (𝐴 = ∅ → ( 𝐴 ∈ V ↔ V ∈ V))
138, 12mtbiri 319 . . 3 (𝐴 = ∅ → ¬ 𝐴 ∈ V)
1413necon2ai 2996 . 2 ( 𝐴 ∈ V → 𝐴 ≠ ∅)
157, 14impbii 201 1 (𝐴 ≠ ∅ ↔ 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 198   = wceq 1507  wex 1742  wcel 2050  wne 2967  Vcvv 3415  wss 3831  c0 4180   cint 4750
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5061
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-v 3417  df-dif 3834  df-in 3838  df-ss 3845  df-nul 4181  df-int 4751
This theorem is referenced by:  intnex  5098  intexab  5099  iinexg  5101  onint0  7329  onintrab  7334  onmindif2  7345  fival  8673  elfi2  8675  elfir  8676  dffi2  8684  elfiun  8691  fifo  8693  tz9.1c  8968  tz9.12lem1  9012  tz9.12lem3  9014  rankf  9019  cardf2  9168  cardval3  9177  cardid2  9178  cardcf  9474  cflim2  9485  intwun  9957  wuncval  9964  inttsk  9996  intgru  10036  gruina  10040  dfrtrcl2  14285  mremre  16736  mrcval  16742  asplss  19826  aspsubrg  19828  toponmre  21408  subbascn  21569  insiga  31041  sigagenval  31044  sigagensiga  31045  dmsigagen  31048  dfon2lem8  32555  dfon2lem9  32556  bj-snmoore  33916  igenval  34781  pclvalN  36471  elrfi  38686  ismrcd1  38690  mzpval  38724  dmmzp  38725  salgenval  42038  intsal  42045
  Copyright terms: Public domain W3C validator