Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isseti Unicode version

Theorem isseti 3115
 Description: A way to say " is a set" (inference rule). (Contributed by NM, 24-Jun-1993.)
Hypothesis
Ref Expression
isseti.1
Assertion
Ref Expression
isseti
Distinct variable group:   ,

Proof of Theorem isseti
StepHypRef Expression
1 isseti.1 . 2
2 isset 3113 . 2
31, 2mpbi 208 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  E.wex 1612  e.wcel 1818   cvv 3109 This theorem is referenced by:  rexcom4b  3131  ceqsex  3145  vtoclf  3160  vtocl2  3162  vtocl3  3163  vtoclef  3182  eqvinc  3226  euind  3286  eusv2nf  4650  zfpair  4689  axpr  4690  opabn0  4783  isarep2  5673  dfoprab2  6343  rnoprab  6385  ov3  6439  omeu  7253  cflem  8647  genpass  9408  supmul1  10533  supmullem2  10535  supmul  10536  uzindOLD  10982  ruclem13  13975  joindm  15633  meetdm  15647  supaddc  30041  supadd  30042  ac6s6f  30581  funressnfv  32213  bnj986  34012  bj-snsetex  34521  elintima  37765 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
 Copyright terms: Public domain W3C validator