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

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

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