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

Metamath Proof Explorer

Theorem ss2rabd

Description: Subclass of a restricted class abstraction (deduction form). Saves ax-10 , ax-11 , ax-12 over using ss2rab and sylibr . (Contributed by SN, 4-Feb-2026)

Ref Expression
Hypothesis ss2rabd.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) )
Assertion ss2rabd ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜒 } )

Proof

Step Hyp Ref Expression
1 ss2rabd.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) )
2 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) )
3 imdistan ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
4 3 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
5 2 4 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
6 1 5 sylib ⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
7 ss2abim ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) } )
8 6 7 syl ⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) } )
9 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) }
10 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜒 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) }
11 8 9 10 3sstr4g ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜒 } )