eqrelf

Description: The equality connective between relations. (Contributed by Peter Mazsa, 25-Jun-2019)

	Ref	Expression
Hypotheses	eqrelf.1	$⊢ \underline{Ⅎ} x A$
	eqrelf.2	$⊢ \underline{Ⅎ} x B$
	eqrelf.3	$⊢ \underline{Ⅎ} y A$
	eqrelf.4	$⊢ \underline{Ⅎ} y B$
Assertion	eqrelf	$⊢ (Rel A \land Rel B) \to (A = B \leftrightarrow \forall x \forall y (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in B))$

Step	Hyp	Ref	Expression
1		eqrelf.1	$⊢ \underline{Ⅎ} x A$
2		eqrelf.2	$⊢ \underline{Ⅎ} x B$
3		eqrelf.3	$⊢ \underline{Ⅎ} y A$
4		eqrelf.4	$⊢ \underline{Ⅎ} y B$
5		eqrel	$⊢ (Rel A \land Rel B) \to (A = B \leftrightarrow \forall u \forall v (⟨u, v⟩ \in A \leftrightarrow ⟨u, v⟩ \in B))$
6		nfv	$⊢ Ⅎ u (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in B)$
7		nfv	$⊢ Ⅎ v (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in B)$
8	1	nfel2	$⊢ Ⅎ x ⟨u, v⟩ \in A$
9	2	nfel2	$⊢ Ⅎ x ⟨u, v⟩ \in B$
10	8 9	nfbi	$⊢ Ⅎ x (⟨u, v⟩ \in A \leftrightarrow ⟨u, v⟩ \in B)$
11	3	nfel2	$⊢ Ⅎ y ⟨u, v⟩ \in A$
12	4	nfel2	$⊢ Ⅎ y ⟨u, v⟩ \in B$
13	11 12	nfbi	$⊢ Ⅎ y (⟨u, v⟩ \in A \leftrightarrow ⟨u, v⟩ \in B)$
14		opeq12	$⊢ (x = u \land y = v) \to ⟨x, y⟩ = ⟨u, v⟩$
15	14	eleq1d	$⊢ (x = u \land y = v) \to (⟨x, y⟩ \in A \leftrightarrow ⟨u, v⟩ \in A)$
16	14	eleq1d	$⊢ (x = u \land y = v) \to (⟨x, y⟩ \in B \leftrightarrow ⟨u, v⟩ \in B)$
17	15 16	bibi12d	$⊢ (x = u \land y = v) \to ((⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in B) \leftrightarrow (⟨u, v⟩ \in A \leftrightarrow ⟨u, v⟩ \in B))$
18	6 7 10 13 17	cbval2v	$⊢ \forall x \forall y (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in B) \leftrightarrow \forall u \forall v (⟨u, v⟩ \in A \leftrightarrow ⟨u, v⟩ \in B)$
19	5 18	bitr4di	$⊢ (Rel A \land Rel B) \to (A = B \leftrightarrow \forall x \forall y (⟨x, y⟩ \in A \leftrightarrow ⟨x, y⟩ \in B))$

Metamath Proof Explorer