releldmqs

Description: Elementhood in the domain quotient of a relation. (Contributed by Peter Mazsa, 24-Apr-2021)

		Ref	Expression
	Assertion	releldmqs	$⊢ A \in V \to (Rel R \to (A \in (dom R / R) \leftrightarrow \exists u \in dom R \exists x \in [u] R A = [u] R))$

Step	Hyp	Ref	Expression
1		resdm	$⊢ Rel R \to {R ↾}_{dom R} = R$
2	1	dmqseqd	$⊢ Rel R \to dom ({R ↾}_{dom R}) / ({R ↾}_{dom R}) = dom R / R$
3	2	eleq2d	$⊢ Rel R \to (A \in (dom ({R ↾}_{dom R}) / ({R ↾}_{dom R})) \leftrightarrow A \in (dom R / R))$
4	3	adantl	$⊢ (A \in V \land Rel R) \to (A \in (dom ({R ↾}_{dom R}) / ({R ↾}_{dom R})) \leftrightarrow A \in (dom R / R))$
5		eldmqsres2	$⊢ A \in V \to (A \in (dom ({R ↾}_{dom R}) / ({R ↾}_{dom R})) \leftrightarrow \exists u \in dom R \exists x \in [u] R A = [u] R)$
6	5	adantr	$⊢ (A \in V \land Rel R) \to (A \in (dom ({R ↾}_{dom R}) / ({R ↾}_{dom R})) \leftrightarrow \exists u \in dom R \exists x \in [u] R A = [u] R)$
7	4 6	bitr3d	$⊢ (A \in V \land Rel R) \to (A \in (dom R / R) \leftrightarrow \exists u \in dom R \exists x \in [u] R A = [u] R)$
8	7	ex	$⊢ A \in V \to (Rel R \to (A \in (dom R / R) \leftrightarrow \exists u \in dom R \exists x \in [u] R A = [u] R))$

Metamath Proof Explorer