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	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑖 𝐵
2		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑖 / 𝑥 ⦌ 𝐵
3		csbeq1a	⊢ ( 𝑥 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
4	1 2 3	cbvdisj	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
5		csbeq1	⊢ ( 𝑖 = 𝑗 → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 = ⦋ 𝑗 / 𝑥 ⦌ 𝐵 )
6	5	disjor	⊢ ( Disj 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
7	4 6	bitri	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )