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

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 ⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) )