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 2110 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2110 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust 1890), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab 2104.
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 2104. (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 1465 | . 2 wff 𝐴 ∈ 𝐵 |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1315 | . . . . 5 class 𝑥 |
6 | 5, 1 | wceq 1316 | . . . 4 wff 𝑥 = 𝐴 |
7 | 5, 2 | wcel 1465 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 103 | . . 3 wff (𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | wex 1453 | . 2 wff ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
10 | 3, 9 | wb 104 | 1 wff (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: eleq1w 2178 eleq2w 2179 eleq1 2180 eleq2 2181 clelab 2242 clabel 2243 nfel 2267 nfeld 2274 sbabel 2284 risset 2440 isset 2666 elex 2671 sbcabel 2962 ssel 3061 disjsn 3555 mptpreima 5002 |
Copyright terms: Public domain | W3C validator |