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

Theorem isseti 2528
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 2526 . 2 (A V ↔ x x = A)
31, 2mpbi 133 1 x x = A
Colors of variables: wff set class
Syntax hints:   = wceq 1219  wex 1350   wcel 1362  Vcvv 2522
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 1305  ax-gen 1307  ax-ie1 1351  ax-ie2 1352  ax-8 1364  ax-4 1369  ax-17 1388  ax-i9 1392  ax-ial 1396  ax-ext 1991
This theorem depends on definitions:  df-bi 110  df-sb 1615  df-clab 1996  df-cleq 2002  df-clel 2005  df-v 2524
This theorem is referenced by:  rexcom4b  2543  ceqsex  2556  vtoclf  2571  vtocl2  2573  vtocl3  2574  vtoclef  2590  eqvinc  2631  euind  2692  opabm  3976  eusv2nf  4122  limom  4247  isarep2  4896  dfoprab2  5459  rnoprab  5494  dmaddpq  6220  dmmulpq  6221  bj-inf2vnlem1  7426
  Copyright terms: Public domain W3C validator