Theorem isseti 2563

Description: A way to say "𝐴 is a set" (inference rule). (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 2561	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
3	1, 2	mpbi 133	1 ⊢ ∃𝑥 𝑥 = 𝐴

Syntax hints:   = wceq 1243  ∃wex 1381   ∈ wcel 1393  Vcvv 2557

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-v 2559

This theorem is referenced by:  rexcom4b  2579  ceqsex  2592  vtoclf  2607  vtocl2  2609  vtocl3  2610  vtoclef  2626  eqvinc  2667  euind  2728  opabm  4017  eusv2nf  4188  limom  4336  isarep2  4986  dfoprab2  5552  rnoprab  5587  dmaddpq  6477  dmmulpq  6478  bj-inf2vnlem1  10095