ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elisset Structured version   GIF version

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

Proof of Theorem elisset
StepHypRef Expression
1 elex 2530 . 2 (A 𝑉A V)
2 isset 2526 . 2 (A V ↔ x x = A)
31, 2sylib 127 1 (A 𝑉x x = A)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1219  wex 1350   wcel 1362  Vcvv 2522
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1305  ax-gen 1307  ax-ie1 1351  ax-ie2 1352  ax-8 1364  ax-4 1369  ax-17 1388  ax-i9 1392  ax-ial 1396  ax-ext 1991
This theorem depends on definitions:  df-bi 110  df-sb 1615  df-clab 1996  df-cleq 2002  df-clel 2005  df-v 2524
This theorem is referenced by:  elex22  2533  elex2  2534  ceqsalt  2544  ceqsalg  2546  cgsexg  2553  cgsex2g  2554  cgsex4g  2555  vtoclgft  2568  vtocleg  2588  vtoclegft  2589  spc2egv  2606  spc2gv  2607  spc3egv  2608  spc3gv  2609  eqvincg  2632  tpid3g  3442  iinexgm  3867  copsex2t  3941  copsex2g  3942  ralxfr2d  4130  rexxfr2d  4131  fliftf  5348  eloprabga  5498  ovmpt4g  5530  eroveu  6092  genpassl  6361  genpassu  6362  bj-inex  7364
  Copyright terms: Public domain W3C validator