Theorem eqrelf

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

	Ref	Expression
Hypotheses	eqrelf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	eqrelf.2	$$⊢\underset{\_}{Ⅎ}xB$$
	eqrelf.3	$$⊢\underset{\_}{Ⅎ}yA$$
	eqrelf.4	$$⊢\underset{\_}{Ⅎ}yB$$
Assertion	eqrelf	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)\to \left(A=B\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in A\leftrightarrow ⟨x,y⟩\in B\right)\right)$$

Proof

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