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	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	disjorsf	$$⊢\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		disjorsf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}iB$$
3		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋i/x⦌B$$
4		csbeq1a	$$⊢x=i\to B=⦋i/x⦌B$$
5	1 2 3 4	cbvdisjf	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \underset{i\in A}{Disj}⦋i/x⦌B$$
6		csbeq1	$$⊢i=j\to ⦋i/x⦌B=⦋j/x⦌B$$
7	6	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)$$
8	5 7	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)$$