eldmcoss2

Description: Elementhood in the domain of cosets. (Contributed by Peter Mazsa, 28-Dec-2018)

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

Step	Hyp	Ref	Expression
1		eldmcoss	$⊢ A \in V \to (A \in dom ≀ R \leftrightarrow \exists u u R A)$
2		brcoss	$⊢ (A \in V \land A \in V) \to (A ≀ R A \leftrightarrow \exists u (u R A \land u R A))$
3	2	anidms	$⊢ A \in V \to (A ≀ R A \leftrightarrow \exists u (u R A \land u R A))$
4		pm4.24	$⊢ u R A \leftrightarrow (u R A \land u R A)$
5	4	exbii	$⊢ \exists u u R A \leftrightarrow \exists u (u R A \land u R A)$
6	3 5	bitr4di	$⊢ A \in V \to (A ≀ R A \leftrightarrow \exists u u R A)$
7	1 6	bitr4d	$⊢ A \in V \to (A \in dom ≀ R \leftrightarrow A ≀ R A)$

Metamath Proof Explorer