This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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