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

Theorem isseti 3337
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 3335 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2mpbi 220 1 𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1620  wex 1841  wcel 2127  Vcvv 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-12 2184  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1623  df-ex 1842  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-v 3330
This theorem is referenced by:  rexcom4b  3355  ceqsex  3369  vtoclf  3386  vtocl  3387  vtocl2  3389  vtocl3  3390  vtoclef  3409  euind  3522  eusv2nf  5001  zfpair  5041  axpr  5042  opabn0  5144  isarep2  6127  dfoprab2  6854  rnoprab  6896  ov3  6950  omeu  7822  cflem  9231  genpass  9994  supaddc  11153  supadd  11154  supmul1  11155  supmullem2  11157  supmul  11158  ruclem13  15141  joindm  17175  meetdm  17189  bnj986  31302  bj-snsetex  33228  bj-restn0  33320  bj-restuni  33327  ac6s6f  34263  elintima  38416  funressnfv  41683  elpglem2  42937
  Copyright terms: Public domain W3C validator