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 2074 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2074 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust 1854), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab 2068.
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 http://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 1433 | . 2 wff 𝐴 ∈ 𝐵 |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1283 | . . . . 5 class 𝑥 |
6 | 5, 1 | wceq 1284 | . . . 4 wff 𝑥 = 𝐴 |
7 | 5, 2 | wcel 1433 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 102 | . . 3 wff (𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | wex 1421 | . 2 wff ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
10 | 3, 9 | wb 103 | 1 wff (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: eleq1 2141 eleq2 2142 clelab 2203 clabel 2204 nfel 2227 nfeld 2234 sbabel 2244 risset 2394 isset 2605 elex 2610 sbcabel 2895 ssel 2993 disjsn 3454 mptpreima 4834 |
Copyright terms: Public domain | W3C validator |