![]() |
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 2170 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2170 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust 2154), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab 2164.
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 2164. (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 2148 | . 2 wff 𝐴 ∈ 𝐵 |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1352 | . . . . 5 class 𝑥 |
6 | 5, 1 | wceq 1353 | . . . 4 wff 𝑥 = 𝐴 |
7 | 5, 2 | wcel 2148 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 104 | . . 3 wff (𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | wex 1492 | . 2 wff ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
10 | 3, 9 | wb 105 | 1 wff (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: eleq1w 2238 eleq2w 2239 eleq1 2240 eleq2 2241 clelab 2303 clabel 2304 nfel 2328 nfeld 2335 sbabel 2346 risset 2505 isset 2743 elex 2748 sbcabel 3044 ssel 3149 disjsn 3654 mptpreima 5122 |
Copyright terms: Public domain | W3C validator |