brxrncnvep

Description: The range product with converse epsilon relation. (Contributed by Peter Mazsa, 22-Jun-2020) (Revised by Peter Mazsa, 22-Nov-2025)

		Ref	Expression
	Assertion	brxrncnvep	$⊢ (A \in V \land B \in W \land C \in X) \to (A R ⋉ E^{-1} ⟨B, C⟩ \leftrightarrow (C \in A \land A R B))$

Step	Hyp	Ref	Expression
1		brxrn	$⊢ (A \in V \land B \in W \land C \in X) \to (A R ⋉ E^{-1} ⟨B, C⟩ \leftrightarrow (A R B \land A E^{-1} C))$
2		brcnvep	$⊢ A \in V \to (A E^{-1} C \leftrightarrow C \in A)$
3	2	anbi1cd	$⊢ A \in V \to ((A R B \land A E^{-1} C) \leftrightarrow (C \in A \land A R B))$
4	3	3ad2ant1	$⊢ (A \in V \land B \in W \land C \in X) \to ((A R B \land A E^{-1} C) \leftrightarrow (C \in A \land A R B))$
5	1 4	bitrd	$⊢ (A \in V \land B \in W \land C \in X) \to (A R ⋉ E^{-1} ⟨B, C⟩ \leftrightarrow (C \in A \land A R B))$

Metamath Proof Explorer