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

Theorem isset 2555
Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 2553) if and only if the class A exists (i.e. there exists some set x equal to class A). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device "A V " to mean "A is a set" very frequently, for example in uniex . Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg , in order to shorten certain proofs we use the more general antecedent A 𝑉 instead of A V to mean "A is a set."

Note that a constant is implicitly considered distinct from all variables. This is why V is not included in the distinct variable list, even though df-clel 2033 requires that the expression substituted for B not contain x. (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
isset (A V ↔ x x = A)
Distinct variable group:   x,A

Proof of Theorem isset
StepHypRef Expression
1 df-clel 2033 . 2 (A V ↔ x(x = A x V))
2 vex 2554 . . . 4 x V
32biantru 286 . . 3 (x = A ↔ (x = A x V))
43exbii 1493 . 2 (x x = Ax(x = A x V))
51, 4bitr4i 176 1 (A V ↔ x x = A)
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98   = 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:  issetf  2556  isseti  2557  issetri  2558  elex  2560  elisset  2562  ceqex  2665  eueq  2706  moeq  2710  mosubt  2712  ru  2757  sbc5  2781  snprc  3426  vprc  3879  vnex  3881  opelopabsb  3988  eusvnfb  4152  dtruex  4237  euiotaex  4826  fvmptdf  5201  fvmptdv2  5203  fmptco  5273  brabvv  5493  ovmpt2df  5574  ovi3  5579  tfrlemibxssdm  5882  freccl  5932  ecexr  6047  bj-vprc  9347  bj-vnex  9349  bj-2inf  9392
  Copyright terms: Public domain W3C validator