Theorem isseti 2811

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

Syntax hints:   = wceq 1397  ∃wex 1540   ∈ wcel 2202  Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  rexcom4b  2828  ceqsex  2841  ceqsexv2d  2843  vtoclf  2857  vtocl2  2859  vtocl3  2860  vtoclef  2879  eqvinc  2929  euind  2993  opabm  4375  eusv2nf  4553  dtruex  4657  limom  4712  isarep2  5417  dfoprab2  6067  rnoprab  6103  dmaddpq  7598  dmmulpq  7599  bj-inf2vnlem1  16565