Metamath Proof Explorer

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 
|- F/_ x A
Assertion disjorsf 
|- ( 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 disjorsf.1 
 |-  F/_ x A
2 nfcv 
 |-  F/_ i B
3 nfcsb1v 
 |-  F/_ x [_ i / x ]_ B
4 csbeq1a 
 |-  ( x = i -> B = [_ i / x ]_ B )
5 1 2 3 4 cbvdisjf 
 |-  ( Disj_ x e. A B <-> Disj_ i e. A [_ i / x ]_ B )
6 csbeq1 
 |-  ( i = j -> [_ i / x ]_ B = [_ j / x ]_ B )
7 6 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 ) = (/) ) )
8 5 7 bitri 
 |-  ( Disj_ x e. A B <-> A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )