Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of TakeutiZaring p. 17. (Contributed by NM, 8-Jan-2002) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 16-May-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfss2 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfcleq | ⊢ ( 𝐴 = ( 𝐴 ∩ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ) | |
| 2 | dfss | ⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝐴 = ( 𝐴 ∩ 𝐵 ) ) | |
| 3 | pm4.71 | ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) ) | |
| 4 | elin | ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) | |
| 5 | 4 | bibi2i | ⊢ ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) ) |
| 6 | 3 5 | bitr4i | ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ) |
| 7 | 6 | albii | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ) |
| 8 | 1 2 7 | 3bitr4i | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) |