Metamath Proof Explorer


Theorem disjorsf

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 _ x A
Assertion disjorsf Disj x A B i A j A i = j i / x B j / x B =

Proof

Step Hyp Ref Expression
1 disjorsf.1 _ x A
2 nfcv _ i B
3 nfcsb1v _ x i / x B
4 csbeq1a x = i B = i / x B
5 1 2 3 4 cbvdisjf Disj x A B Disj i A i / x B
6 csbeq1 i = j i / x B = j / x B
7 6 disjor Disj i A i / x B i A j A i = j i / x B j / x B =
8 5 7 bitri Disj x A B i A j A i = j i / x B j / x B =