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 2033 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2033 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust 1813), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab 2027.
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 | ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | wcel 1393 | . 2 wff 𝐴 ∈ 𝐵 |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1242 | . . . . 5 class 𝑥 |
6 | 5, 1 | wceq 1243 | . . . 4 wff 𝑥 = 𝐴 |
7 | 5, 2 | wcel 1393 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 97 | . . 3 wff (𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | wex 1381 | . 2 wff ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
10 | 3, 9 | wb 98 | 1 wff (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: eleq1 2100 eleq2 2101 clelab 2162 clabel 2163 nfel 2186 nfeld 2193 sbabel 2203 risset 2352 isset 2561 elex 2566 sbcabel 2839 ssel 2939 disjsn 3432 mptpreima 4814 |
Copyright terms: Public domain | W3C validator |