Theorem ecex2

Description: Condition for a coset to be a set. (Contributed by Peter Mazsa, 4-May-2019)

	Ref	Expression
Assertion	ecex2	⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ( 𝐵 ∈ 𝐴 → [ 𝐵 ] 𝑅 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		ecexg	⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ∈ V )
2		ecres2	⊢ ( 𝐵 ∈ 𝐴 → [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) = [ 𝐵 ] 𝑅 )
3	2	eleq1d	⊢ ( 𝐵 ∈ 𝐴 → ( [ 𝐵 ] ( 𝑅 ↾ 𝐴 ) ∈ V ↔ [ 𝐵 ] 𝑅 ∈ V ) )
4	1 3	syl5ibcom	⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ( 𝐵 ∈ 𝐴 → [ 𝐵 ] 𝑅 ∈ V ) )