Theorem isseti 2830

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

Syntax hints:   = wceq 1402  ∃wex 1545   ∈ wcel 2209  Vcvv 2821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is referenced by:  rexcom4b  2847  ceqsex  2860  ceqsexv2d  2862  vtoclf  2876  vtocl2  2878  vtocl3  2879  vtoclef  2898  eqvinc  2949  euind  3013  opabm  4418  eusv2nf  4597  dtruex  4701  limom  4756  isarep2  5463  dfoprab2  6125  rnoprab  6161  dmaddpq  7736  dmmulpq  7737  bj-inf2vnlem1  16910