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

Metamath Proof Explorer

Theorem ss2rab

Description: Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999)

Ref Expression
Assertion ss2rab ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )

Proof

Step Hyp Ref Expression
1 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) }
3 1 2 sseq12i ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } )
4 ss2ab ⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
5 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) )
6 imdistan ⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
7 6 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) )
8 5 7 bitr2i ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )
9 3 4 8 3bitri ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )