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

Syntax Definition cv 1323
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 for justification.

While it is tempting and perhaps occasionally useful to view cv 1323 as a "type conversion" from a set variable to a class variable, keep in mind that cv 1323 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 1325 of predicate calculus from the wceq 1324 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.)

Ref Expression
Ref Expression

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

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