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 2132 it extends or "overloads" the
use of the existing membership symbol, but unlike df-cleq 2132 it does not
strengthen the set of valid wffs of logic when the class variables are
replaced with setvar variables (see cleljust 1910), so we don't include
any set theory axiom as a hypothesis. See also comments about the
syntax under df-clab 2126.
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 2126. (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 1480 | . 2 wff 𝐴 ∈ 𝐵 |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1330 | . . . . 5 class 𝑥 |
6 | 5, 1 | wceq 1331 | . . . 4 wff 𝑥 = 𝐴 |
7 | 5, 2 | wcel 1480 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 103 | . . 3 wff (𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | wex 1468 | . 2 wff ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵) |
10 | 3, 9 | wb 104 | 1 wff (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) |
Colors of variables: wff set class |
This definition is referenced by: eleq1w 2200 eleq2w 2201 eleq1 2202 eleq2 2203 clelab 2265 clabel 2266 nfel 2290 nfeld 2297 sbabel 2307 risset 2463 isset 2692 elex 2697 sbcabel 2990 ssel 3091 disjsn 3585 mptpreima 5032 |
Copyright terms: Public domain | W3C validator |