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

Metamath Proof Explorer

Theorem brcnvg

Description: The converse of a binary relation swaps arguments. Theorem 11 of Suppes p. 61. (Contributed by NM, 10-Oct-2005)

		Ref	Expression
	Assertion	brcnvg	$⊢ (A \in C \land B \in D) \to (A R^{-1} B \leftrightarrow B R A)$

Step	Hyp	Ref	Expression
1		breq2	$⊢ x = A \to (y R x \leftrightarrow y R A)$
2		breq1	$⊢ y = B \to (y R A \leftrightarrow B R A)$
3		df-cnv	$⊢ R^{-1} = \{⟨x, y⟩ \| y R x\}$
4	1 2 3	brabg	$⊢ (A \in C \land B \in D) \to (A R^{-1} B \leftrightarrow B R A)$