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

Theorem isseti 2580
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 2578 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
31, 2mpbi 137 1 𝑥 𝑥 = 𝐴
Colors of variables: wff set class
Syntax hints:   = wceq 1259  wex 1397  wcel 1409  Vcvv 2574
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-v 2576
This theorem is referenced by:  rexcom4b  2596  ceqsex  2609  vtoclf  2624  vtocl2  2626  vtocl3  2627  vtoclef  2643  eqvinc  2690  euind  2751  opabm  4045  eusv2nf  4216  limom  4364  isarep2  5014  dfoprab2  5580  rnoprab  5615  dmaddpq  6535  dmmulpq  6536  bj-inf2vnlem1  10482
  Copyright terms: Public domain W3C validator