elcnv2

Description: Membership in a converse relation. Equation 5 of Suppes p. 62. (Contributed by NM, 11-Aug-2004)

		Ref	Expression
	Assertion	elcnv2	$⊢ A \in R^{-1} \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land ⟨y, x⟩ \in R)$

Step	Hyp	Ref	Expression
1		elcnv	$⊢ A \in R^{-1} \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land y R x)$
2		df-br	$⊢ y R x \leftrightarrow ⟨y, x⟩ \in R$
3	2	anbi2i	$⊢ (A = ⟨x, y⟩ \land y R x) \leftrightarrow (A = ⟨x, y⟩ \land ⟨y, x⟩ \in R)$
4	3	2exbii	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land y R x) \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land ⟨y, x⟩ \in R)$
5	1 4	bitri	$⊢ A \in R^{-1} \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land ⟨y, x⟩ \in R)$

Metamath Proof Explorer