Description: An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993)
Ref | Expression | ||
---|---|---|---|
Hypothesis | clel4.1 | ⊢ 𝐵 ∈ V | |
Assertion | clel4 | ⊢ ( 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐵 → 𝐴 ∈ 𝑥 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clel4.1 | ⊢ 𝐵 ∈ V | |
2 | eleq2 | ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵 ) ) | |
3 | 1 2 | ceqsalv | ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐵 → 𝐴 ∈ 𝑥 ) ↔ 𝐴 ∈ 𝐵 ) |
4 | 3 | bicomi | ⊢ ( 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐵 → 𝐴 ∈ 𝑥 ) ) |