HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem isseti 1806
Description: A way to say "A is a set" (inference rule).
Hypothesis
Ref Expression
isseti.1 |- A e. V
Assertion
Ref Expression
isseti |- E.x x = A
Distinct variable group:   x,A
Proof of Theorem isseti
StepHypRef Expression
1 isseti.1 . 2 |- A e. V
2 isset 1805 . 2 |- (A e. V <-> E.x x = A)
31, 2mpbi 189 1 |- E.x x = A
Colors of variables: wff set class
Syntax hints:   = wceq 953   e. wcel 955  E.wex 977  Vcvv 1802
This theorem is referenced by:  ceqsex 1825  vtoclf 1832  vtocl2 1834  vtocl3 1835  vtoclef 1848  csbie2t 2023  zfpair 2767  axpr 2768  ssopab2 2811  opabn0 2813  funfvop 3788  iinon 3895  dfoprab2 3976  rnoprab 3989  2ndconst 4081  cflem 4877  genpdm 5077  genpn0 5078  genpass 5084  reclem3pr 5130  elreal 5222  nn1suc 5887  uzindOLD 6156  infcvglem1 7156
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803
Copyright terms: Public domain