![]() |
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 2093 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2093 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust 1873), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab 2087.
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 https://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 1448 | . 2 wff 𝐴 ∈ 𝐵 |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1298 | . . . . 5 class 𝑥 |
6 | 5, 1 | wceq 1299 | . . . 4 wff 𝑥 = 𝐴 |
7 | 5, 2 | wcel 1448 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 103 | . . 3 wff (𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | wex 1436 | . 2 wff ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
10 | 3, 9 | wb 104 | 1 wff (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: eleq1w 2160 eleq2w 2161 eleq1 2162 eleq2 2163 clelab 2224 clabel 2225 nfel 2249 nfeld 2256 sbabel 2266 risset 2422 isset 2647 elex 2652 sbcabel 2942 ssel 3041 disjsn 3532 mptpreima 4968 |
Copyright terms: Public domain | W3C validator |