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