Theorem ss2abim

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

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

Proof

Step	Hyp	Ref	Expression
1		spsbim	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
2	1	alrimiv	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
3		df-ss	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) )
4		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
5		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 )
6	4 5	imbi12i	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
7	6	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
8	3 7	bitr2i	⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } )
9	2 8	sylib	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } )