Description: Two ways to say that a collection B ( i ) for i e. A is disjoint. (Contributed by Thierry Arnoux, 8-Mar-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | disjorsf.1 | ||
Assertion | disjorsf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjorsf.1 | ||
2 | nfcv | ||
3 | nfcsb1v | ||
4 | csbeq1a | ||
5 | 1 2 3 4 | cbvdisjf | |
6 | csbeq1 | ||
7 | 6 | disjor | |
8 | 5 7 | bitri |