Description: If from the two propositions that every result of an application of the procedure R to B has property f and that property f is hereditary in the R -sequence, it can be inferred, whatever f may be, that E has property f , then we say E follows B in the R -sequence. Definition 76 of Frege1879 p. 60.
Each of B , E and R must be sets. (Contributed by RP, 2-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | frege76.b | ||
frege76.e | |||
frege76.r | |||
Assertion | dffrege76 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frege76.b | ||
2 | frege76.e | ||
3 | frege76.r | ||
4 | brtrclfv2 | ||
5 | 1 2 3 4 | mp3an | |
6 | 2 | elexi | |
7 | 6 | elintab | |
8 | imaundi | ||
9 | 8 | equncomi | |
10 | 9 | sseq1i | |
11 | unss | ||
12 | 10 11 | bitr4i | |
13 | df-he | ||
14 | 13 | bicomi | |
15 | dfss2 | ||
16 | 1 | elexi | |
17 | vex | ||
18 | 16 17 | elimasn | |
19 | df-br | ||
20 | 18 19 | bitr4i | |
21 | 20 | imbi1i | |
22 | 21 | albii | |
23 | 15 22 | bitri | |
24 | 14 23 | anbi12i | |
25 | 12 24 | bitri | |
26 | 25 | imbi1i | |
27 | impexp | ||
28 | 26 27 | bitri | |
29 | 28 | albii | |
30 | 5 7 29 | 3bitrri |