ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cv Unicode version

Syntax Definition cv 1382
Description: This syntax construction states that a variable , which has been declared to be a set variable by $f statement vx, is also a class expression. See comments in set.mm for justification.

While it is tempting and perhaps occasionally useful to view cv 1382 as a "type conversion" from a set variable to a class variable, keep in mind that cv 1382 is intrinsically no different from any other class-building syntax.

(The description above applies to set theory, not predicate calculus. The purpose of introducing here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1384 of predicate calculus from the wceq 1383 of set theory, so that we don't "overload" the connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers.)

Hypothesis
Ref Expression
vx
Assertion
Ref Expression
cv

This syntax is primitive. The first axiom using it is ax-8 1387.

Colors of variables: wff set class
  Copyright terms: Public domain W3C validator