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

Theorem isseti 2557
 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 2555 . 2 (A V ↔ x x = A)
31, 2mpbi 133 1 x x = A
 Colors of variables: wff set class Syntax hints:   = wceq 1242  ∃wex 1378   ∈ wcel 1390  Vcvv 2551 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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-ext 2019 This theorem depends on definitions:  df-bi 110  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-v 2553 This theorem is referenced by:  rexcom4b  2573  ceqsex  2586  vtoclf  2601  vtocl2  2603  vtocl3  2604  vtoclef  2620  eqvinc  2661  euind  2722  opabm  4008  eusv2nf  4154  limom  4279  isarep2  4929  dfoprab2  5494  rnoprab  5529  dmaddpq  6363  dmmulpq  6364  bj-inf2vnlem1  9430
 Copyright terms: Public domain W3C validator