Theorem isseti 3182

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

Step	Hyp	Ref	Expression
1		isseti.1	. 2 ⊢ 𝐴 ∈ V
2		isset 3180	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	mpbi 219	1 ⊢ ∃𝑥 𝑥 = 𝐴

Syntax hints:   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  rexcom4b  3200  ceqsex  3214  vtoclf  3231  vtocl  3232  vtocl2  3234  vtocl3  3235  vtoclef  3254  eqvinc  3300  euind  3360  eusv2nf  4790  zfpair  4831  axpr  4832  opabn0  4931  isarep2  5892  dfoprab2  6599  rnoprab  6641  ov3  6695  omeu  7552  cflem  8951  genpass  9710  supaddc  10867  supadd  10868  supmul1  10869  supmullem2  10871  supmul  10872  ruclem13  14810  joindm  16826  meetdm  16840  bnj986  30278  bj-snsetex  32144  bj-restn0  32224  bj-restuni  32231  ac6s6f  33151  elintima  36964  funressnfv  39857  elpglem2  42254