Step | Hyp | Ref
| Expression |
1 | | sprsymrelf.p |
. . . 4
Pairs |
2 | | sprsymrelf.r |
. . . 4
|
3 | | sprsymrelf.f |
. . . 4
|
4 | 1, 2, 3 | sprsymrelf 41745 |
. . 3
|
5 | 4 | a1i 11 |
. 2
|
6 | | breq 4655 |
. . . . . . . . 9
|
7 | | breq 4655 |
. . . . . . . . 9
|
8 | 6, 7 | bibi12d 335 |
. . . . . . . 8
|
9 | 8 | 2ralbidv 2989 |
. . . . . . 7
|
10 | 9, 2 | elrab2 3366 |
. . . . . 6
|
11 | | eqid 2622 |
. . . . . . . . . . 11
Pairs
Pairs
|
12 | 11 | sprsymrelfolem1 41742 |
. . . . . . . . . 10
Pairs
Pairs |
13 | 12, 1 | eleqtrri 2700 |
. . . . . . . . 9
Pairs
|
14 | 13 | a1i 11 |
. . . . . . . 8
Pairs
|
15 | | rexeq 3139 |
. . . . . . . . . . 11
Pairs
Pairs
|
16 | 15 | opabbidv 4716 |
. . . . . . . . . 10
Pairs
Pairs
|
17 | 16 | eqeq2d 2632 |
. . . . . . . . 9
Pairs
Pairs
|
18 | 17 | adantl 482 |
. . . . . . . 8
Pairs
Pairs
|
19 | | selpw 4165 |
. . . . . . . . . 10
|
20 | | xpss 5226 |
. . . . . . . . . . . . . . . 16
|
21 | | sstr2 3610 |
. . . . . . . . . . . . . . . 16
|
22 | 20, 21 | mpi 20 |
. . . . . . . . . . . . . . 15
|
23 | | df-rel 5121 |
. . . . . . . . . . . . . . 15
|
24 | 22, 23 | sylibr 224 |
. . . . . . . . . . . . . 14
|
25 | 24 | adantl 482 |
. . . . . . . . . . . . 13
|
26 | | dfrel4v 5584 |
. . . . . . . . . . . . . 14
|
27 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 27, 28 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
|
30 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . 20
|
31 | | nfra2 2946 |
. . . . . . . . . . . . . . . . . . . 20
|
32 | 30, 31 | nfan 1828 |
. . . . . . . . . . . . . . . . . . 19
|
33 | 11 | sprsymrelfolem2 41743 |
. . . . . . . . . . . . . . . . . . . 20
Pairs
|
34 | 33 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . 19
Pairs
|
35 | 29, 32, 34 | opabbid 4715 |
. . . . . . . . . . . . . . . . . 18
Pairs
|
36 | 35 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
Pairs
|
37 | 36 | biimpd 219 |
. . . . . . . . . . . . . . . 16
Pairs
|
38 | 37 | ex 450 |
. . . . . . . . . . . . . . 15
Pairs
|
39 | 38 | com23 86 |
. . . . . . . . . . . . . 14
Pairs
|
40 | 26, 39 | syl5bi 232 |
. . . . . . . . . . . . 13
Pairs
|
41 | 25, 40 | mpd 15 |
. . . . . . . . . . . 12
Pairs
|
42 | 41 | expcom 451 |
. . . . . . . . . . 11
Pairs
|
43 | 42 | com23 86 |
. . . . . . . . . 10
Pairs
|
44 | 19, 43 | sylbi 207 |
. . . . . . . . 9
Pairs
|
45 | 44 | imp31 448 |
. . . . . . . 8
Pairs
|
46 | 14, 18, 45 | rspcedvd 3317 |
. . . . . . 7
|
47 | 46 | ex 450 |
. . . . . 6
|
48 | 10, 47 | sylbi 207 |
. . . . 5
|
49 | 48 | impcom 446 |
. . . 4
|
50 | 1, 2, 3 | sprsymrelfv 41744 |
. . . . . . 7
|
51 | 50 | adantl 482 |
. . . . . 6
|
52 | 51 | eqeq2d 2632 |
. . . . 5
|
53 | 52 | rexbidva 3049 |
. . . 4
|
54 | 49, 53 | mpbird 247 |
. . 3
|
55 | 54 | ralrimiva 2966 |
. 2
|
56 | | dffo3 6374 |
. 2
|
57 | 5, 55, 56 | sylanbrc 698 |
1
|