relbrcnvg

Description: When R is a relation, the sethood assumptions on brcnv can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	relbrcnvg	$⊢ Rel R \to (A R^{-1} B \leftrightarrow B R A)$

Step	Hyp	Ref	Expression
1		relcnv	$⊢ Rel R^{-1}$
2	1	brrelex12i	$⊢ A R^{-1} B \to (A \in V \land B \in V)$
3	2	a1i	$⊢ Rel R \to (A R^{-1} B \to (A \in V \land B \in V))$
4		brrelex12	$⊢ (Rel R \land B R A) \to (B \in V \land A \in V)$
5	4	ancomd	$⊢ (Rel R \land B R A) \to (A \in V \land B \in V)$
6	5	ex	$⊢ Rel R \to (B R A \to (A \in V \land B \in V))$
7		brcnvg	$⊢ (A \in V \land B \in V) \to (A R^{-1} B \leftrightarrow B R A)$
8	7	a1i	$⊢ Rel R \to ((A \in V \land B \in V) \to (A R^{-1} B \leftrightarrow B R A))$
9	3 6 8	pm5.21ndd	$⊢ Rel R \to (A R^{-1} B \leftrightarrow B R A)$

Metamath Proof Explorer