Description: Alternate definition of subclass relationship: a class A is a subclass of another class B iff each element of A is equal to an element of B . (Contributed by AV, 13-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | dfss5 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑦 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfss3 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) | |
2 | clel5 | ⊢ ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑦 ) | |
3 | 2 | ralbii | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑦 ) |
4 | 1 3 | bitri | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑦 ) |