Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  isseti GIF version

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
StepHypRef Expression
1 isseti.1 . 2 𝐴 ∈ V
2 isset 2561 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2mpbi 133 1 𝑥 𝑥 = 𝐴
 Colors of variables: wff set class 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
 Copyright terms: Public domain W3C validator