Theorem opeldifid

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

	Ref	Expression
Assertion	opeldifid	|- ( Rel A -> ( <. X , Y >. e. ( A \ _I ) <-> ( <. X , Y >. e. A /\ X =/= Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		reldif	|- ( Rel A -> Rel ( A \ _I ) )
2		brrelex2	|- ( ( Rel ( A \ _I ) /\ X ( A \ _I ) Y ) -> Y e. _V )
3	1 2	sylan	|- ( ( Rel A /\ X ( A \ _I ) Y ) -> Y e. _V )
4		brrelex2	|- ( ( Rel A /\ X A Y ) -> Y e. _V )
5	4	adantrr	|- ( ( Rel A /\ ( X A Y /\ X =/= Y ) ) -> Y e. _V )
6		brdif	|- ( X ( A \ _I ) Y <-> ( X A Y /\ -. X _I Y ) )
7		ideqg	|- ( Y e. _V -> ( X _I Y <-> X = Y ) )
8	7	necon3bbid	|- ( Y e. _V -> ( -. X _I Y <-> X =/= Y ) )
9	8	anbi2d	|- ( Y e. _V -> ( ( X A Y /\ -. X _I Y ) <-> ( X A Y /\ X =/= Y ) ) )
10	6 9	bitrid	|- ( Y e. _V -> ( X ( A \ _I ) Y <-> ( X A Y /\ X =/= Y ) ) )
11	3 5 10	pm5.21nd	|- ( Rel A -> ( X ( A \ _I ) Y <-> ( X A Y /\ X =/= Y ) ) )
12		df-br	|- ( X ( A \ _I ) Y <-> <. X , Y >. e. ( A \ _I ) )
13		df-br	|- ( X A Y <-> <. X , Y >. e. A )
14	13	anbi1i	|- ( ( X A Y /\ X =/= Y ) <-> ( <. X , Y >. e. A /\ X =/= Y ) )
15	11 12 14	3bitr3g	|- ( Rel A -> ( <. X , Y >. e. ( A \ _I ) <-> ( <. X , Y >. e. A /\ X =/= Y ) ) )