Theorem ss2abim

Description: Class abstractions in a subclass relationship. Reverse direction of ss2ab which requires fewer axioms. (Contributed by SN, 22-Dec-2024)

	Ref	Expression
Assertion	ss2abim	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } )

Proof

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