Theorem disjors

Description: Two ways to say that a collection B ( i ) for i e. A is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	disjors	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall i\in A\forall j\in A\left(i=j\vee ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfcv	$$⊢\underset{\_}{Ⅎ}iB$$
2		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋i/x⦌B$$
3		csbeq1a	$$⊢x=i\to B=⦋i/x⦌B$$
4	1 2 3	cbvdisj	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \underset{i\in A}{Disj}⦋i/x⦌B$$
5		csbeq1	$$⊢i=j\to ⦋i/x⦌B=⦋j/x⦌B$$
6	5	disjor	$$⊢\underset{i\in A}{Disj}⦋i/x⦌B\leftrightarrow \forall i\in A\forall j\in A\left(i=j\vee ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)$$
7	4 6	bitri	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall i\in A\forall j\in A\left(i=j\vee ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)$$