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

Step	Hyp	Ref	Expression
1		isseti.1	. 2
2		isset 3113	. 2
3	1, 2	mpbi 208	1

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