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

Metamath Proof Explorer

Theorem ssrabdv

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 31-Aug-2006)

Ref Expression
Hypotheses ssrabdv.1 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
ssrabdv.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜓 )
Assertion ssrabdv ( 𝜑 → 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )

Proof

Step Hyp Ref Expression
1 ssrabdv.1 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
2 ssrabdv.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜓 )
3 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝜓 )
4 ssrab ⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜓 ) )
5 1 3 4 sylanbrc ⊢ ( 𝜑 → 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )