This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ecelqsdmb

Description: R -coset of B in a quotient set, biconditional version. (Contributed by Peter Mazsa, 17-Apr-2019) (Revised by Peter Mazsa, 22-Nov-2025)

Ref Expression
Assertion ecelqsdmb ⊢ R ↾ A ∈ V ∧ dom ⁡ R = A → B R ∈ A / R ↔ B ∈ A

Proof

Step Hyp Ref Expression
1 ecelqsdm ⊢ dom ⁡ R = A ∧ B R ∈ A / R → B ∈ A
2 1 ex ⊢ dom ⁡ R = A → B R ∈ A / R → B ∈ A
3 2 adantl ⊢ R ↾ A ∈ V ∧ dom ⁡ R = A → B R ∈ A / R → B ∈ A
4 ecelqs ⊢ R ↾ A ∈ V ∧ B ∈ A → B R ∈ A / R
5 4 ex ⊢ R ↾ A ∈ V → B ∈ A → B R ∈ A / R
6 5 adantr ⊢ R ↾ A ∈ V ∧ dom ⁡ R = A → B ∈ A → B R ∈ A / R
7 3 6 impbid ⊢ R ↾ A ∈ V ∧ dom ⁡ R = A → B R ∈ A / R ↔ B ∈ A