![]() |
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 2133 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2133 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust 1911), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab 2127.
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 2127. (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 1481 | . 2 wff 𝐴 ∈ 𝐵 |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1331 | . . . . 5 class 𝑥 |
6 | 5, 1 | wceq 1332 | . . . 4 wff 𝑥 = 𝐴 |
7 | 5, 2 | wcel 1481 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 103 | . . 3 wff (𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | wex 1469 | . 2 wff ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
10 | 3, 9 | wb 104 | 1 wff (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: eleq1w 2201 eleq2w 2202 eleq1 2203 eleq2 2204 clelab 2266 clabel 2267 nfel 2291 nfeld 2298 sbabel 2308 risset 2466 isset 2695 elex 2700 sbcabel 2994 ssel 3096 disjsn 3593 mptpreima 5040 |
Copyright terms: Public domain | W3C validator |