Theorem abssi

Description: Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006)

	Ref	Expression
Hypothesis	abssi.1	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
Assertion	abssi	⊢ { 𝑥 ∣ 𝜑 } ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		abssi.1	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
2	1	ss2abi	⊢ { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝑥 ∈ 𝐴 }
3		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 } = 𝐴
4	2 3	sseqtri	⊢ { 𝑥 ∣ 𝜑 } ⊆ 𝐴