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

Metamath Proof Explorer

Theorem eldmcnv

Description: Elementhood in a domain of a converse. (Contributed by Peter Mazsa, 25-May-2018)

		Ref	Expression
	Assertion	eldmcnv	$⊢ A \in V \to (A \in dom R^{-1} \leftrightarrow \exists u u R A)$

Step	Hyp	Ref	Expression
1		eldmg	$⊢ A \in V \to (A \in dom R^{-1} \leftrightarrow \exists u A R^{-1} u)$
2		brcnvg	$⊢ (A \in V \land u \in V) \to (A R^{-1} u \leftrightarrow u R A)$
3	2	elvd	$⊢ A \in V \to (A R^{-1} u \leftrightarrow u R A)$
4	3	exbidv	$⊢ A \in V \to (\exists u A R^{-1} u \leftrightarrow \exists u u R A)$
5	1 4	bitrd	$⊢ A \in V \to (A \in dom R^{-1} \leftrightarrow \exists u u R A)$