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 ( ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 ∧ dom 𝑅 = 𝐴 ) → ( [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ↔ 𝐵 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ecelqsdm ⊢ ( ( dom 𝑅 = 𝐴 ∧ [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ) → 𝐵 ∈ 𝐴 )
2 1 ex ⊢ ( dom 𝑅 = 𝐴 → ( [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) → 𝐵 ∈ 𝐴 ) )
3 2 adantl ⊢ ( ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 ∧ dom 𝑅 = 𝐴 ) → ( [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) → 𝐵 ∈ 𝐴 ) )
4 ecelqs ⊢ ( ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 ∧ 𝐵 ∈ 𝐴 ) → [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )
5 4 ex ⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ( 𝐵 ∈ 𝐴 → [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ) )
6 5 adantr ⊢ ( ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 ∧ dom 𝑅 = 𝐴 ) → ( 𝐵 ∈ 𝐴 → [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ) )
7 3 6 impbid ⊢ ( ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 ∧ dom 𝑅 = 𝐴 ) → ( [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ↔ 𝐵 ∈ 𝐴 ) )