This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eldmcoss

Description: Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 29-Mar-2019)

		Ref	Expression
	Assertion	eldmcoss	$⊢ A \in V \to (A \in dom ≀ R \leftrightarrow \exists u u R A)$

Step	Hyp	Ref	Expression
1		dmcoss3	$⊢ dom ≀ R = dom R^{-1}$
2	1	eleq2i	$⊢ A \in dom ≀ R \leftrightarrow A \in dom R^{-1}$
3		eldmcnv	$⊢ A \in V \to (A \in dom R^{-1} \leftrightarrow \exists u u R A)$
4	2 3	bitrid	$⊢ A \in V \to (A \in dom ≀ R \leftrightarrow \exists u u R A)$