br1cnvres

Description: Binary relation on the converse of a restriction. (Contributed by Peter Mazsa, 27-Jul-2019)

		Ref	Expression
	Assertion	br1cnvres	$⊢ B \in V \to (B {({R ↾}_{A})}^{-1} C \leftrightarrow (C \in A \land C R B))$

Step	Hyp	Ref	Expression
1		df-res	$⊢ {R ↾}_{A} = R \cap (A \times V)$
2	1	cnveqi	$⊢ {({R ↾}_{A})}^{-1} = {(R \cap (A \times V))}^{-1}$
3	2	breqi	$⊢ B {({R ↾}_{A})}^{-1} C \leftrightarrow B {(R \cap (A \times V))}^{-1} C$
4		elex	$⊢ B \in V \to B \in V$
5		br1cnvinxp	$⊢ B {(R \cap (A \times V))}^{-1} C \leftrightarrow ((B \in V \land C \in A) \land C R B)$
6		anass	$⊢ ((B \in V \land C \in A) \land C R B) \leftrightarrow (B \in V \land (C \in A \land C R B))$
7	5 6	bitri	$⊢ B {(R \cap (A \times V))}^{-1} C \leftrightarrow (B \in V \land (C \in A \land C R B))$
8	7	baib	$⊢ B \in V \to (B {(R \cap (A \times V))}^{-1} C \leftrightarrow (C \in A \land C R B))$
9	4 8	syl	$⊢ B \in V \to (B {(R \cap (A \times V))}^{-1} C \leftrightarrow (C \in A \land C R B))$
10	3 9	bitrid	$⊢ B \in V \to (B {({R ↾}_{A})}^{-1} C \leftrightarrow (C \in A \land C R B))$

Metamath Proof Explorer