Metamath Proof Explorer

Theorem elecex

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

Ref Expression
Assertion elecex ⊢ R ↾ A ∈ V → B ∈ A → B R ∈ V

Proof

Step Hyp Ref Expression
1 ecexg ⊢ R ↾ A ∈ V → B R ↾ A ∈ V
2 elecreseq ⊢ B ∈ A → B R ↾ A = B R
3 2 eleq1d ⊢ B ∈ A → B R ↾ A ∈ V ↔ B R ∈ V
4 1 3 syl5ibcom ⊢ R ↾ A ∈ V → B ∈ A → B R ∈ V