Theorem ss2ab

Description: Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994)

	Ref	Expression
Assertion	ss2ab	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
2		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜓 }
3	1 2	dfss2f	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } → 𝑥 ∈ { 𝑥 ∣ 𝜓 } ) )
4		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
5		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜓 )
6	4 5	imbi12i	⊢ ( ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } → 𝑥 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ( 𝜑 → 𝜓 ) )
7	6	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } → 𝑥 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ∀ 𝑥 ( 𝜑 → 𝜓 ) )
8	3 7	bitri	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝜑 → 𝜓 ) )