Metamath Proof Explorer

Theorem ecelqs

Description: Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 22-Nov-2025)

		Ref	Expression
	Assertion	ecelqs	$⊢ ({R ↾}_{A} \in V \land B \in A) \to [B] R \in (A / R)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ [B] R = [B] R$
2		eceq1	$⊢ x = B \to [x] R = [B] R$
3	2	rspceeqv	$⊢ (B \in A \land [B] R = [B] R) \to \exists x \in A [B] R = [x] R$
4	1 3	mpan2	$⊢ B \in A \to \exists x \in A [B] R = [x] R$
5	4	adantl	$⊢ ({R ↾}_{A} \in V \land B \in A) \to \exists x \in A [B] R = [x] R$
6		elecex	$⊢ {R ↾}_{A} \in V \to (B \in A \to [B] R \in V)$
7	6	imp	$⊢ ({R ↾}_{A} \in V \land B \in A) \to [B] R \in V$
8		elqsg	$⊢ [B] R \in V \to ([B] R \in (A / R) \leftrightarrow \exists x \in A [B] R = [x] R)$
9	7 8	syl	$⊢ ({R ↾}_{A} \in V \land B \in A) \to ([B] R \in (A / R) \leftrightarrow \exists x \in A [B] R = [x] R)$
10	5 9	mpbird	$⊢ ({R ↾}_{A} \in V \land B \in A) \to [B] R \in (A / R)$