Theorem qsss

Description: A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypothesis	qsss.1	⊢ ( 𝜑 → 𝑅 Er 𝐴 )
Assertion	qsss	⊢ ( 𝜑 → ( 𝐴 / 𝑅 ) ⊆ 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		qsss.1	⊢ ( 𝜑 → 𝑅 Er 𝐴 )
2		vex	⊢ 𝑥 ∈ V
3	2	elqs	⊢ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 = [ 𝑦 ] 𝑅 )
4	1	ecss	⊢ ( 𝜑 → [ 𝑦 ] 𝑅 ⊆ 𝐴 )
5		sseq1	⊢ ( 𝑥 = [ 𝑦 ] 𝑅 → ( 𝑥 ⊆ 𝐴 ↔ [ 𝑦 ] 𝑅 ⊆ 𝐴 ) )
6	4 5	syl5ibrcom	⊢ ( 𝜑 → ( 𝑥 = [ 𝑦 ] 𝑅 → 𝑥 ⊆ 𝐴 ) )
7		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
8	6 7	imbitrrdi	⊢ ( 𝜑 → ( 𝑥 = [ 𝑦 ] 𝑅 → 𝑥 ∈ 𝒫 𝐴 ) )
9	8	rexlimdvw	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = [ 𝑦 ] 𝑅 → 𝑥 ∈ 𝒫 𝐴 ) )
10	3 9	biimtrid	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 / 𝑅 ) → 𝑥 ∈ 𝒫 𝐴 ) )
11	10	ssrdv	⊢ ( 𝜑 → ( 𝐴 / 𝑅 ) ⊆ 𝒫 𝐴 )