Step |
Hyp |
Ref |
Expression |
1 |
|
elreal |
|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A ) |
2 |
|
elreal |
|- ( B e. RR <-> E. y e. R. <. y , 0R >. = B ) |
3 |
|
breq1 |
|- ( <. x , 0R >. = A -> ( <. x , 0R >. . <-> A . ) ) |
4 |
|
eqeq1 |
|- ( <. x , 0R >. = A -> ( <. x , 0R >. = <. y , 0R >. <-> A = <. y , 0R >. ) ) |
5 |
|
breq2 |
|- ( <. x , 0R >. = A -> ( <. y , 0R >. . <-> <. y , 0R >. |
6 |
4 5
|
orbi12d |
|- ( <. x , 0R >. = A -> ( ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) <-> ( A = <. y , 0R >. \/ <. y , 0R >. |
7 |
6
|
notbid |
|- ( <. x , 0R >. = A -> ( -. ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) <-> -. ( A = <. y , 0R >. \/ <. y , 0R >. |
8 |
3 7
|
bibi12d |
|- ( <. x , 0R >. = A -> ( ( <. x , 0R >. . <-> -. ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) ) <-> ( A . <-> -. ( A = <. y , 0R >. \/ <. y , 0R >. |
9 |
|
breq2 |
|- ( <. y , 0R >. = B -> ( A . <-> A |
10 |
|
eqeq2 |
|- ( <. y , 0R >. = B -> ( A = <. y , 0R >. <-> A = B ) ) |
11 |
|
breq1 |
|- ( <. y , 0R >. = B -> ( <. y , 0R >. B |
12 |
10 11
|
orbi12d |
|- ( <. y , 0R >. = B -> ( ( A = <. y , 0R >. \/ <. y , 0R >. ( A = B \/ B |
13 |
12
|
notbid |
|- ( <. y , 0R >. = B -> ( -. ( A = <. y , 0R >. \/ <. y , 0R >. -. ( A = B \/ B |
14 |
9 13
|
bibi12d |
|- ( <. y , 0R >. = B -> ( ( A . <-> -. ( A = <. y , 0R >. \/ <. y , 0R >. ( A -. ( A = B \/ B |
15 |
|
ltsosr |
|- |
16 |
|
sotric |
|- ( ( ( x -. ( x = y \/ y |
17 |
15 16
|
mpan |
|- ( ( x e. R. /\ y e. R. ) -> ( x -. ( x = y \/ y |
18 |
|
ltresr |
|- ( <. x , 0R >. . <-> x |
19 |
|
vex |
|- x e. _V |
20 |
19
|
eqresr |
|- ( <. x , 0R >. = <. y , 0R >. <-> x = y ) |
21 |
|
ltresr |
|- ( <. y , 0R >. . <-> y |
22 |
20 21
|
orbi12i |
|- ( ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) <-> ( x = y \/ y |
23 |
22
|
notbii |
|- ( -. ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) <-> -. ( x = y \/ y |
24 |
17 18 23
|
3bitr4g |
|- ( ( x e. R. /\ y e. R. ) -> ( <. x , 0R >. . <-> -. ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) ) ) |
25 |
1 2 8 14 24
|
2gencl |
|- ( ( A e. RR /\ B e. RR ) -> ( A -. ( A = B \/ B |