Theorem isseti 2649

Description: A way to say "𝐴 is a set" (inference form). (Contributed by NM, 5-Aug-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 2647	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	mpbi 144	1 ⊢ ∃𝑥 𝑥 = 𝐴

Syntax hints:   = wceq 1299  ∃wex 1436   ∈ wcel 1448  Vcvv 2641

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-v 2643

This theorem is referenced by:  rexcom4b  2666  ceqsex  2679  vtoclf  2694  vtocl2  2696  vtocl3  2697  vtoclef  2714  eqvinc  2762  euind  2824  opabm  4140  eusv2nf  4315  dtruex  4412  limom  4465  isarep2  5146  dfoprab2  5750  rnoprab  5786  dmaddpq  7088  dmmulpq  7089  bj-inf2vnlem1  12753