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 ) = (/) ) )