Description: A closed form of tfis . (Contributed by Scott Fenton, 8-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | tfisg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrab2 | |
|
2 | dfss3 | |
|
3 | nfcv | |
|
4 | 3 | elrabsf | |
5 | 4 | simprbi | |
6 | 5 | ralimi | |
7 | 2 6 | sylbi | |
8 | nfcv | |
|
9 | nfsbc1v | |
|
10 | 8 9 | nfralw | |
11 | nfsbc1v | |
|
12 | 10 11 | nfim | |
13 | raleq | |
|
14 | sbceq1a | |
|
15 | 13 14 | imbi12d | |
16 | 12 15 | rspc | |
17 | 16 | impcom | |
18 | 7 17 | syl5 | |
19 | simpr | |
|
20 | 18 19 | jctild | |
21 | 3 | elrabsf | |
22 | 20 21 | syl6ibr | |
23 | 22 | ralrimiva | |
24 | tfi | |
|
25 | 1 23 24 | sylancr | |
26 | 25 | eqcomd | |
27 | rabid2 | |
|
28 | 26 27 | sylib | |