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

Theorem isseti 3403
Description: A way to say "𝐴 is a set" (inference form). (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 3401 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2mpbi 221 1 𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wex 1859  wcel 2156  Vcvv 3391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-tru 1641  df-ex 1860  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-v 3393
This theorem is referenced by:  rexcom4b  3421  ceqsex  3435  vtoclf  3451  vtocl  3452  vtocl2  3454  vtocl3  3455  vtoclef  3474  euind  3591  eusv2nf  5064  zfpair  5094  axpr  5095  opabn0  5201  isarep2  6185  dfoprab2  6927  rnoprab  6969  ov3  7023  omeu  7898  cflem  9349  genpass  10112  supaddc  11271  supadd  11272  supmul1  11273  supmullem2  11275  supmul  11276  ruclem13  15187  joindm  17204  meetdm  17218  bnj986  31342  bj-snsetex  33256  bj-restn0  33349  bj-restuni  33356  ac6s6f  34286  elintima  38439  funressnfv  41656  elpglem2  43020
  Copyright terms: Public domain W3C validator