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
|
syl5bb |
|- ( 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 ) ) ) |