![]() |
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 2182 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2182 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust 2166), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab 2176.
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 2176. (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 2160 | . 2 wff 𝐴 ∈ 𝐵 |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1363 | . . . . 5 class 𝑥 |
6 | 5, 1 | wceq 1364 | . . . 4 wff 𝑥 = 𝐴 |
7 | 5, 2 | wcel 2160 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 104 | . . 3 wff (𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | wex 1503 | . 2 wff ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
10 | 3, 9 | wb 105 | 1 wff (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: eleq1w 2250 eleq2w 2251 eleq1 2252 eleq2 2253 clelab 2315 clabel 2316 nfel 2341 nfeld 2348 sbabel 2359 risset 2518 isset 2758 elex 2763 sbcabel 3059 ssel 3164 disjsn 3669 mptpreima 5137 |
Copyright terms: Public domain | W3C validator |