Metamath Proof Explorer


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 𝑥𝐴 𝐵 ↔ ∀ 𝑖𝐴𝑗𝐴 ( 𝑖 = 𝑗 ∨ ( 𝑖 / 𝑥 𝐵 𝑗 / 𝑥 𝐵 ) = ∅ ) )