Description: Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ssabf.1 | ⊢ Ⅎ 𝑥 𝐴 | |
Assertion | ssabf | ⊢ ( 𝐴 ⊆ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssabf.1 | ⊢ Ⅎ 𝑥 𝐴 | |
2 | 1 | abid2f | ⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 } = 𝐴 |
3 | 2 | sseq1i | ⊢ ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } ⊆ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ⊆ { 𝑥 ∣ 𝜑 } ) |
4 | ss2ab | ⊢ ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } ⊆ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |
5 | 3 4 | bitr3i | ⊢ ( 𝐴 ⊆ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |