Metamath Proof Explorer


Theorem ssrabf

Description: Subclass of a restricted class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses ssrabf.1 𝑥 𝐵
ssrabf.2 𝑥 𝐴
Assertion ssrabf ( 𝐵 ⊆ { 𝑥𝐴𝜑 } ↔ ( 𝐵𝐴 ∧ ∀ 𝑥𝐵 𝜑 ) )

Proof

Step Hyp Ref Expression
1 ssrabf.1 𝑥 𝐵
2 ssrabf.2 𝑥 𝐴
3 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
4 3 sseq2i ( 𝐵 ⊆ { 𝑥𝐴𝜑 } ↔ 𝐵 ⊆ { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } )
5 1 ssabf ( 𝐵 ⊆ { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } ↔ ∀ 𝑥 ( 𝑥𝐵 → ( 𝑥𝐴𝜑 ) ) )
6 1 2 dfss3f ( 𝐵𝐴 ↔ ∀ 𝑥𝐵 𝑥𝐴 )
7 6 anbi1i ( ( 𝐵𝐴 ∧ ∀ 𝑥𝐵 𝜑 ) ↔ ( ∀ 𝑥𝐵 𝑥𝐴 ∧ ∀ 𝑥𝐵 𝜑 ) )
8 r19.26 ( ∀ 𝑥𝐵 ( 𝑥𝐴𝜑 ) ↔ ( ∀ 𝑥𝐵 𝑥𝐴 ∧ ∀ 𝑥𝐵 𝜑 ) )
9 df-ral ( ∀ 𝑥𝐵 ( 𝑥𝐴𝜑 ) ↔ ∀ 𝑥 ( 𝑥𝐵 → ( 𝑥𝐴𝜑 ) ) )
10 7 8 9 3bitr2ri ( ∀ 𝑥 ( 𝑥𝐵 → ( 𝑥𝐴𝜑 ) ) ↔ ( 𝐵𝐴 ∧ ∀ 𝑥𝐵 𝜑 ) )
11 4 5 10 3bitri ( 𝐵 ⊆ { 𝑥𝐴𝜑 } ↔ ( 𝐵𝐴 ∧ ∀ 𝑥𝐵 𝜑 ) )