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

Theorem elisset 3210
Description: An element of a class exists. (Contributed by NM, 1-May-1995.)
Assertion
Ref Expression
elisset (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem elisset
StepHypRef Expression
1 elex 3207 . 2 (𝐴𝑉𝐴 ∈ V)
2 isset 3202 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2sylib 208 1 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wex 1702  wcel 1988  Vcvv 3195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-12 2045  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1484  df-ex 1703  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-v 3197
This theorem is referenced by:  elex2  3211  elex22  3212  ceqsalt  3223  ceqsalgALT  3226  cgsexg  3233  cgsex2g  3234  cgsex4g  3235  vtoclgft  3249  vtoclgftOLD  3250  vtocleg  3274  vtoclegft  3275  spc2egv  3290  spc3egv  3292  tpid3gOLD  4297  iinexg  4815  ralxfr2d  4873  copsex2t  4947  copsex2g  4948  fliftf  6550  eloprabga  6732  ovmpt4g  6768  eroveu  7827  mreiincl  16237  metustfbas  22343  spc2ed  29282  eqvincg  29284  brabgaf  29392  bnj852  30965  bnj938  30981  bnj1125  31034  bnj1148  31038  bnj1154  31041  bj-csbsnlem  32873  bj-snsetex  32926  bj-snglc  32932  elex2VD  38893  elex22VD  38894  tpid3gVD  38897  elsprel  41490
  Copyright terms: Public domain W3C validator