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

Theorem isseti 3199
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 3197 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2mpbi 220 1 𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wex 1701  wcel 1987  Vcvv 3190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1483  df-ex 1702  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3192
This theorem is referenced by:  rexcom4b  3217  ceqsex  3231  vtoclf  3248  vtocl  3249  vtocl2  3251  vtocl3  3252  vtoclef  3271  eqvinc  3318  euind  3380  eusv2nf  4834  zfpair  4875  axpr  4876  opabn0  4976  isarep2  5946  dfoprab2  6666  rnoprab  6708  ov3  6762  omeu  7625  cflem  9028  genpass  9791  supaddc  10950  supadd  10951  supmul1  10952  supmullem2  10954  supmul  10955  ruclem13  14915  joindm  16943  meetdm  16957  bnj986  30785  bj-snsetex  32651  bj-restn0  32733  bj-restuni  32740  ac6s6f  33652  elintima  37465  funressnfv  40542  elpglem2  41778
  Copyright terms: Public domain W3C validator