Theorem ss2ab1

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	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		spsbim	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( [ 𝑡 / 𝑥 ] 𝜑 → [ 𝑡 / 𝑥 ] 𝜓 ) )
2		df-clab	⊢ ( 𝑡 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑡 / 𝑥 ] 𝜑 )
3		df-clab	⊢ ( 𝑡 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑡 / 𝑥 ] 𝜓 )
4	1 2 3	3imtr4g	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝑡 ∈ { 𝑥 ∣ 𝜑 } → 𝑡 ∈ { 𝑥 ∣ 𝜓 } ) )
5	4	ssrdv	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } )