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_ x e. A B <-> A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )

Proof

Step Hyp Ref Expression
1 nfcv
 |-  F/_ i B
2 nfcsb1v
 |-  F/_ x [_ i / x ]_ B
3 csbeq1a
 |-  ( x = i -> B = [_ i / x ]_ B )
4 1 2 3 cbvdisj
 |-  ( Disj_ x e. A B <-> Disj_ i e. A [_ i / x ]_ B )
5 csbeq1
 |-  ( i = j -> [_ i / x ]_ B = [_ j / x ]_ B )
6 5 disjor
 |-  ( Disj_ i e. A [_ i / x ]_ B <-> A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
7 4 6 bitri
 |-  ( Disj_ x e. A B <-> A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )