Description: Class abstractions in a subclass relationship, closed form. One direction of ss2ab using fewer axioms. (Contributed by SN, 22-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | ss2ab1 | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spsbim | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( [ 𝑡 / 𝑥 ] 𝜑 → [ 𝑡 / 𝑥 ] 𝜓 ) ) | |
2 | df-clab | ⊢ ( 𝑡 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑡 / 𝑥 ] 𝜑 ) | |
3 | df-clab | ⊢ ( 𝑡 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑡 / 𝑥 ] 𝜓 ) | |
4 | 1 2 3 | 3imtr4g | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝑡 ∈ { 𝑥 ∣ 𝜑 } → 𝑡 ∈ { 𝑥 ∣ 𝜓 } ) ) |
5 | 4 | ssrdv | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } ) |