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

Proof

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