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

Theorem isseti 3240
 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 3238 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2mpbi 220 1 𝑥 𝑥 = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1523  ∃wex 1744   ∈ wcel 2030  Vcvv 3231 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233 This theorem is referenced by:  rexcom4b  3258  ceqsex  3272  vtoclf  3289  vtocl  3290  vtocl2  3292  vtocl3  3293  vtoclef  3312  euind  3426  eusv2nf  4894  zfpair  4934  axpr  4935  opabn0  5035  isarep2  6016  dfoprab2  6743  rnoprab  6785  ov3  6839  omeu  7710  cflem  9106  genpass  9869  supaddc  11028  supadd  11029  supmul1  11030  supmullem2  11032  supmul  11033  ruclem13  15015  joindm  17050  meetdm  17064  bnj986  31150  bj-snsetex  33076  bj-restn0  33168  bj-restuni  33175  ac6s6f  34111  elintima  38262  funressnfv  41529  elpglem2  42783
 Copyright terms: Public domain W3C validator