Step |
Hyp |
Ref |
Expression |
1 |
|
impexp |
|- ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> ( <. x , y >. e. F -> ( <. x , z >. e. F -> y = z ) ) ) |
2 |
1
|
albii |
|- ( A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> A. z ( <. x , y >. e. F -> ( <. x , z >. e. F -> y = z ) ) ) |
3 |
|
19.21v |
|- ( A. z ( <. x , y >. e. F -> ( <. x , z >. e. F -> y = z ) ) <-> ( <. x , y >. e. F -> A. z ( <. x , z >. e. F -> y = z ) ) ) |
4 |
|
vex |
|- x e. _V |
5 |
|
vex |
|- y e. _V |
6 |
4 5
|
opelco |
|- ( <. x , y >. e. ( ( _V \ _I ) o. F ) <-> E. z ( x F z /\ z ( _V \ _I ) y ) ) |
7 |
|
df-br |
|- ( x F z <-> <. x , z >. e. F ) |
8 |
|
brv |
|- z _V y |
9 |
|
brdif |
|- ( z ( _V \ _I ) y <-> ( z _V y /\ -. z _I y ) ) |
10 |
8 9
|
mpbiran |
|- ( z ( _V \ _I ) y <-> -. z _I y ) |
11 |
5
|
ideq |
|- ( z _I y <-> z = y ) |
12 |
|
equcom |
|- ( z = y <-> y = z ) |
13 |
11 12
|
bitri |
|- ( z _I y <-> y = z ) |
14 |
10 13
|
xchbinx |
|- ( z ( _V \ _I ) y <-> -. y = z ) |
15 |
7 14
|
anbi12i |
|- ( ( x F z /\ z ( _V \ _I ) y ) <-> ( <. x , z >. e. F /\ -. y = z ) ) |
16 |
15
|
exbii |
|- ( E. z ( x F z /\ z ( _V \ _I ) y ) <-> E. z ( <. x , z >. e. F /\ -. y = z ) ) |
17 |
|
exanali |
|- ( E. z ( <. x , z >. e. F /\ -. y = z ) <-> -. A. z ( <. x , z >. e. F -> y = z ) ) |
18 |
6 16 17
|
3bitri |
|- ( <. x , y >. e. ( ( _V \ _I ) o. F ) <-> -. A. z ( <. x , z >. e. F -> y = z ) ) |
19 |
18
|
con2bii |
|- ( A. z ( <. x , z >. e. F -> y = z ) <-> -. <. x , y >. e. ( ( _V \ _I ) o. F ) ) |
20 |
|
opex |
|- <. x , y >. e. _V |
21 |
|
eldif |
|- ( <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) <-> ( <. x , y >. e. _V /\ -. <. x , y >. e. ( ( _V \ _I ) o. F ) ) ) |
22 |
20 21
|
mpbiran |
|- ( <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) <-> -. <. x , y >. e. ( ( _V \ _I ) o. F ) ) |
23 |
19 22
|
bitr4i |
|- ( A. z ( <. x , z >. e. F -> y = z ) <-> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) ) |
24 |
23
|
imbi2i |
|- ( ( <. x , y >. e. F -> A. z ( <. x , z >. e. F -> y = z ) ) <-> ( <. x , y >. e. F -> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) ) ) |
25 |
2 3 24
|
3bitri |
|- ( A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> ( <. x , y >. e. F -> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) ) ) |
26 |
25
|
2albii |
|- ( A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> A. x A. y ( <. x , y >. e. F -> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) ) ) |
27 |
|
ssrel |
|- ( Rel F -> ( F C_ ( _V \ ( ( _V \ _I ) o. F ) ) <-> A. x A. y ( <. x , y >. e. F -> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) ) ) ) |
28 |
26 27
|
bitr4id |
|- ( Rel F -> ( A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> F C_ ( _V \ ( ( _V \ _I ) o. F ) ) ) ) |
29 |
28
|
pm5.32i |
|- ( ( Rel F /\ A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) <-> ( Rel F /\ F C_ ( _V \ ( ( _V \ _I ) o. F ) ) ) ) |
30 |
|
dffun4 |
|- ( Fun F <-> ( Rel F /\ A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) ) |
31 |
|
sscoid |
|- ( F C_ ( _I o. ( _V \ ( ( _V \ _I ) o. F ) ) ) <-> ( Rel F /\ F C_ ( _V \ ( ( _V \ _I ) o. F ) ) ) ) |
32 |
29 30 31
|
3bitr4i |
|- ( Fun F <-> F C_ ( _I o. ( _V \ ( ( _V \ _I ) o. F ) ) ) ) |