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

Theorem isseti 3181
Description: A way to say "𝐴 is a set" (inference rule). (Contributed by NM, 24-Jun-1993.)
Hypothesis
Ref Expression
isseti.1 𝐴 ∈ V
Assertion
Ref Expression
isseti 𝑥 𝑥 = 𝐴
Distinct variable group:   𝑥,𝐴

Proof of Theorem isseti
StepHypRef Expression
1 isseti.1 . 2 𝐴 ∈ V
2 isset 3179 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2mpbi 218 1 𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wex 1694  wcel 1976  Vcvv 3172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-v 3174
This theorem is referenced by:  rexcom4b  3199  ceqsex  3213  vtoclf  3230  vtocl  3231  vtocl2  3233  vtocl3  3234  vtoclef  3253  eqvinc  3299  euind  3359  eusv2nf  4785  zfpair  4826  axpr  4827  opabn0  4921  isarep2  5878  dfoprab2  6577  rnoprab  6619  ov3  6673  omeu  7530  cflem  8929  genpass  9688  supaddc  10840  supadd  10841  supmul1  10842  supmullem2  10844  supmul  10845  ruclem13  14759  joindm  16775  meetdm  16789  bnj986  30112  bj-snsetex  31968  bj-restn0  32048  bj-restuni  32055  ac6s6f  32975  elintima  36788  funressnfv  39681
  Copyright terms: Public domain W3C validator