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

Theorem isseti 3494
Description: A way to say "𝐴 is a set" (inference form). (Contributed by NM, 24-Jun-1993.) Remove dependencies on axioms. (Revised by BJ, 13-Jul-2019.)
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 elisset 3491 . 2 (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴)
31, 2ax-mp 5 1 𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wex 1781  wcel 2115  Vcvv 3480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896
This theorem is referenced by:  rexcom4b  3510  ceqsex  3526  vtoclf  3544  vtocl  3545  vtocl2OLD  3548  vtoclef  3569  euind  3701  eusv2nf  5283  zfpair  5309  axprALT  5310  opabn0  5427  isarep2  6431  dfoprab2  7205  rnoprab  7250  ov3  7305  omeu  8207  cflem  9666  genpass  10429  supaddc  11604  supadd  11605  supmul1  11606  supmullem2  11608  supmul  11609  ruclem13  15595  joindm  17613  meetdm  17627  bnj986  32287  satfdm  32676  fmla0  32689  fmlasuc0  32691  dmscut  33332  bj-snsetex  34346  bj-restn0  34452  bj-restuni  34459  ac6s6f  35559  elintima  40274  funressnfv  43565  elpglem2  45171
  Copyright terms: Public domain W3C validator