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} \in V \land dom R = A) \to ([B] R \in (A / R) \leftrightarrow B \in A)$

Proof

Step	Hyp	Ref	Expression
1		ecelqsdm	$⊢ (dom R = A \land [B] R \in (A / R)) \to B \in A$
2	1	ex	$⊢ dom R = A \to ([B] R \in (A / R) \to B \in A)$
3	2	adantl	$⊢ ({R ↾}_{A} \in V \land dom R = A) \to ([B] R \in (A / R) \to B \in A)$
4		ecelqs	$⊢ ({R ↾}_{A} \in V \land B \in A) \to [B] R \in (A / R)$
5	4	ex	$⊢ {R ↾}_{A} \in V \to (B \in A \to [B] R \in (A / R))$
6	5	adantr	$⊢ ({R ↾}_{A} \in V \land dom R = A) \to (B \in A \to [B] R \in (A / R))$
7	3 6	impbid	$⊢ ({R ↾}_{A} \in V \land dom R = A) \to ([B] R \in (A / R) \leftrightarrow B \in A)$