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

Theorem isseti 2540
Description: A way to say "A is a set" (inference rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
isseti.1 A V
Assertion
Ref Expression
isseti x x = A
Distinct variable group:   x,A

Proof of Theorem isseti
StepHypRef Expression
1 isseti.1 . 2 A V
2 isset 2538 . 2 (A V ↔ x x = A)
31, 2mpbi 133 1 x x = A
Colors of variables: wff set class
Syntax hints:  wex 1362   = wceq 1374   wcel 1376  Vcvv 2534
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-4 1383  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-v 2536
This theorem is referenced by:  rexcom4b  2555  ceqsex  2568  vtoclf  2583  vtocl2  2585  vtocl3  2586  vtoclef  2602  eqvinc  2643  euind  2704  opabm  3971  eusv2nf  4114  limom  4239  isarep2  4889  dfoprab2  5454  rnoprab  5489  ov3  5539
  Copyright terms: Public domain W3C validator