![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-clel | GIF version |
Description: Define the membership
connective between classes. Theorem 6.3 of
[Quine] p. 41, or Proposition 4.6 of [TakeutiZaring] p. 13, which we
adopt as a definition. See these references for its metalogical
justification. Note that like df-cleq 2030 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2030 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust 1810), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab 2024.
This is called the "axiom of membership" by [Levy] p. 338, who treats the theory of classes as an extralogical extension to our logic and set theory axioms. For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-clel | ⊢ (A ∈ B ↔ ∃x(x = A ∧ x ∈ B)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | 1, 2 | wcel 1390 | . 2 wff A ∈ B |
4 | vx | . . . . . 6 setvar x | |
5 | 4 | cv 1241 | . . . . 5 class x |
6 | 5, 1 | wceq 1242 | . . . 4 wff x = A |
7 | 5, 2 | wcel 1390 | . . . 4 wff x ∈ B |
8 | 6, 7 | wa 97 | . . 3 wff (x = A ∧ x ∈ B) |
9 | 8, 4 | wex 1378 | . 2 wff ∃x(x = A ∧ x ∈ B) |
10 | 3, 9 | wb 98 | 1 wff (A ∈ B ↔ ∃x(x = A ∧ x ∈ B)) |
Colors of variables: wff set class |
This definition is referenced by: eleq1 2097 eleq2 2098 clelab 2159 clabel 2160 nfel 2183 nfeld 2190 sbabel 2200 risset 2346 isset 2555 elex 2560 sbcabel 2833 ssel 2933 disjsn 3423 mptpreima 4757 |
Copyright terms: Public domain | W3C validator |