Metamath Proof Explorer


Theorem ss2rabdf

Description: Deduction of restricted abstraction subclass from implication. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses ss2rabdf.1 𝑥 𝜑
ss2rabdf.2 ( ( 𝜑𝑥𝐴 ) → ( 𝜓𝜒 ) )
Assertion ss2rabdf ( 𝜑 → { 𝑥𝐴𝜓 } ⊆ { 𝑥𝐴𝜒 } )

Proof

Step Hyp Ref Expression
1 ss2rabdf.1 𝑥 𝜑
2 ss2rabdf.2 ( ( 𝜑𝑥𝐴 ) → ( 𝜓𝜒 ) )
3 2 ex ( 𝜑 → ( 𝑥𝐴 → ( 𝜓𝜒 ) ) )
4 1 3 ralrimi ( 𝜑 → ∀ 𝑥𝐴 ( 𝜓𝜒 ) )
5 ss2rab ( { 𝑥𝐴𝜓 } ⊆ { 𝑥𝐴𝜒 } ↔ ∀ 𝑥𝐴 ( 𝜓𝜒 ) )
6 4 5 sylibr ( 𝜑 → { 𝑥𝐴𝜓 } ⊆ { 𝑥𝐴𝜒 } )