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

Metamath Proof Explorer

Theorem ssrabdf

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by Glauco Siliprandi, 5-Jan-2025)

Ref Expression
Hypotheses ssrabdf.1 ⊢ Ⅎ 𝑥 𝐴
ssrabdf.2 ⊢ Ⅎ 𝑥 𝐵
ssrabdf.3 ⊢ Ⅎ 𝑥 𝜑
ssrabdf.4 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
ssrabdf.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜓 )
Assertion ssrabdf ( 𝜑 → 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )

Proof

Step Hyp Ref Expression
1 ssrabdf.1 ⊢ Ⅎ 𝑥 𝐴
2 ssrabdf.2 ⊢ Ⅎ 𝑥 𝐵
3 ssrabdf.3 ⊢ Ⅎ 𝑥 𝜑
4 ssrabdf.4 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
5 ssrabdf.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜓 )
6 3 5 ralrimia ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝜓 )
7 2 1 ssrabf ⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜓 ) )
8 4 6 7 sylanbrc ⊢ ( 𝜑 → 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )