Theorem isseti 3209

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 3207	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	mpbi 220	1 ⊢ ∃𝑥 𝑥 = 𝐴

Syntax hints:   = wceq 1483  ∃wex 1704   ∈ wcel 1990  Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  rexcom4b  3227  ceqsex  3241  vtoclf  3258  vtocl  3259  vtocl2  3261  vtocl3  3262  vtoclef  3281  euind  3393  eusv2nf  4864  zfpair  4904  axpr  4905  opabn0  5006  isarep2  5978  dfoprab2  6701  rnoprab  6743  ov3  6797  omeu  7665  cflem  9068  genpass  9831  supaddc  10990  supadd  10991  supmul1  10992  supmullem2  10994  supmul  10995  ruclem13  14971  joindm  17003  meetdm  17017  bnj986  31024  bj-snsetex  32951  bj-restn0  33043  bj-restuni  33050  ac6s6f  33981  elintima  37945  funressnfv  41208  elpglem2  42455