Theorem opeldifid

Description: Ordered pair elementhood outside of the diagonal. (Contributed by Thierry Arnoux, 1-Jan-2020)

	Ref	Expression
Assertion	opeldifid	$$⊢\mathrm{Rel}A\to \left(⟨X,Y⟩\in \left(A\setminus \mathrm{I}\right)\leftrightarrow \left(⟨X,Y⟩\in A\wedge X\ne Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		reldif	$$⊢\mathrm{Rel}A\to \mathrm{Rel}\left(A\setminus \mathrm{I}\right)$$
2		brrelex2	$$⊢\left(\mathrm{Rel}\left(A\setminus \mathrm{I}\right)\wedge X\left(A\setminus \mathrm{I}\right)Y\right)\to Y\in \mathrm{V}$$
3	1 2	sylan	$$⊢\left(\mathrm{Rel}A\wedge X\left(A\setminus \mathrm{I}\right)Y\right)\to Y\in \mathrm{V}$$
4		brrelex2	$$⊢\left(\mathrm{Rel}A\wedge XAY\right)\to Y\in \mathrm{V}$$
5	4	adantrr	$$⊢\left(\mathrm{Rel}A\wedge \left(XAY\wedge X\ne Y\right)\right)\to Y\in \mathrm{V}$$
6		brdif	$$⊢X\left(A\setminus \mathrm{I}\right)Y\leftrightarrow \left(XAY\wedge \neg X\mathrm{I}Y\right)$$
7		ideqg	$$⊢Y\in \mathrm{V}\to \left(X\mathrm{I}Y\leftrightarrow X=Y\right)$$
8	7	necon3bbid	$$⊢Y\in \mathrm{V}\to \left(\neg X\mathrm{I}Y\leftrightarrow X\ne Y\right)$$
9	8	anbi2d	$$⊢Y\in \mathrm{V}\to \left(\left(XAY\wedge \neg X\mathrm{I}Y\right)\leftrightarrow \left(XAY\wedge X\ne Y\right)\right)$$
10	6 9	bitrid	$$⊢Y\in \mathrm{V}\to \left(X\left(A\setminus \mathrm{I}\right)Y\leftrightarrow \left(XAY\wedge X\ne Y\right)\right)$$
11	3 5 10	pm5.21nd	$$⊢\mathrm{Rel}A\to \left(X\left(A\setminus \mathrm{I}\right)Y\leftrightarrow \left(XAY\wedge X\ne Y\right)\right)$$
12		df-br	$$⊢X\left(A\setminus \mathrm{I}\right)Y\leftrightarrow ⟨X,Y⟩\in \left(A\setminus \mathrm{I}\right)$$
13		df-br	$$⊢XAY\leftrightarrow ⟨X,Y⟩\in A$$
14	13	anbi1i	$$⊢\left(XAY\wedge X\ne Y\right)\leftrightarrow \left(⟨X,Y⟩\in A\wedge X\ne Y\right)$$
15	11 12 14	3bitr3g	$$⊢\mathrm{Rel}A\to \left(⟨X,Y⟩\in \left(A\setminus \mathrm{I}\right)\leftrightarrow \left(⟨X,Y⟩\in A\wedge X\ne Y\right)\right)$$