Metamath Proof Explorer

Theorem disjunsn

Description: Append an element to a disjoint collection. Similar to ralunsn , gsumunsn , etc. (Contributed by Thierry Arnoux, 28-Mar-2018)

Ref Expression
Hypothesis disjunsn.s 
|- ( x = M -> B = C )
Assertion disjunsn 
|- ( ( M e. V /\ -. M e. A ) -> ( Disj_ x e. ( A u. { M } ) B <-> ( Disj_ x e. A B /\ ( U_ x e. A B i^i C ) = (/) ) ) )

Proof

Step Hyp Ref Expression
1 disjunsn.s 
 |-  ( x = M -> B = C )
2 disjors 
 |-  ( Disj_ x e. ( A u. { M } ) B <-> A. i e. ( A u. { M } ) A. j e. ( A u. { M } ) ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
3 eqeq1 
 |-  ( i = M -> ( i = j <-> M = j ) )
4 csbeq1 
 |-  ( i = M -> [_ i / x ]_ B = [_ M / x ]_ B )
5 4 ineq1d 
 |-  ( i = M -> ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = ( [_ M / x ]_ B i^i [_ j / x ]_ B ) )
6 5 eqeq1d 
 |-  ( i = M -> ( ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
7 3 6 orbi12d 
 |-  ( i = M -> ( ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) )
8 7 ralbidv 
 |-  ( i = M -> ( A. j e. ( A u. { M } ) ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> A. j e. ( A u. { M } ) ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) )
9 8 ralunsn 
 |-  ( M e. V -> ( A. i e. ( A u. { M } ) A. j e. ( A u. { M } ) ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> ( A. i e. A A. j e. ( A u. { M } ) ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ A. j e. ( A u. { M } ) ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) ) )
10 2 9 syl5bb 
 |-  ( M e. V -> ( Disj_ x e. ( A u. { M } ) B <-> ( A. i e. A A. j e. ( A u. { M } ) ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ A. j e. ( A u. { M } ) ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) ) )
11 eqeq2 
 |-  ( j = M -> ( i = j <-> i = M ) )
12 csbeq1 
 |-  ( j = M -> [_ j / x ]_ B = [_ M / x ]_ B )
13 12 ineq2d 
 |-  ( j = M -> ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = ( [_ i / x ]_ B i^i [_ M / x ]_ B ) )
14 13 eqeq1d 
 |-  ( j = M -> ( ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
15 11 14 orbi12d 
 |-  ( j = M -> ( ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) )
16 15 ralunsn 
 |-  ( M e. V -> ( A. j e. ( A u. { M } ) ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> ( A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) ) )
17 16 ralbidv 
 |-  ( M e. V -> ( A. i e. A A. j e. ( A u. { M } ) ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> A. i e. A ( A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) ) )
18 eqeq2 
 |-  ( j = M -> ( M = j <-> M = M ) )
19 12 ineq2d 
 |-  ( j = M -> ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = ( [_ M / x ]_ B i^i [_ M / x ]_ B ) )
20 19 eqeq1d 
 |-  ( j = M -> ( ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> ( [_ M / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
21 18 20 orbi12d 
 |-  ( j = M -> ( ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> ( M = M \/ ( [_ M / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) )
22 21 ralunsn 
 |-  ( M e. V -> ( A. j e. ( A u. { M } ) ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> ( A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ ( M = M \/ ( [_ M / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) ) )
23 eqid 
 |-  M = M
24 23 orci 
 |-  ( M = M \/ ( [_ M / x ]_ B i^i [_ M / x ]_ B ) = (/) )
25 24 biantru 
 |-  ( A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> ( A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ ( M = M \/ ( [_ M / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) )
26 22 25 bitr4di 
 |-  ( M e. V -> ( A. j e. ( A u. { M } ) ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) )
27 17 26 anbi12d 
 |-  ( M e. V -> ( ( A. i e. A A. j e. ( A u. { M } ) ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ A. j e. ( A u. { M } ) ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) <-> ( A. i e. A ( A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) /\ A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) ) )
28 10 27 bitrd 
 |-  ( M e. V -> ( Disj_ x e. ( A u. { M } ) B <-> ( A. i e. A ( A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) /\ A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) ) )
29 r19.26 
 |-  ( A. i e. A ( A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) <-> ( A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) )
30 disjors 
 |-  ( Disj_ x e. A B <-> A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
31 30 anbi1i 
 |-  ( ( Disj_ x e. A B /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) <-> ( A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) )
32 29 31 bitr4i 
 |-  ( A. i e. A ( A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) <-> ( Disj_ x e. A B /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) )
33 32 anbi1i 
 |-  ( ( A. i e. A ( A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) /\ ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) /\ A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) <-> ( ( Disj_ x e. A B /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) /\ A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) )
34 28 33 bitrdi 
 |-  ( M e. V -> ( Disj_ x e. ( A u. { M } ) B <-> ( ( Disj_ x e. A B /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) /\ A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) ) )
35 34 adantr 
 |-  ( ( M e. V /\ -. M e. A ) -> ( Disj_ x e. ( A u. { M } ) B <-> ( ( Disj_ x e. A B /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) /\ A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) ) )
36 orcom 
 |-  ( ( ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) \/ i = M ) <-> ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
37 36 ralbii 
 |-  ( A. i e. A ( ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) \/ i = M ) <-> A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
38 r19.30 
 |-  ( A. i e. A ( ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) \/ i = M ) -> ( A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) \/ E. i e. A i = M ) )
39 risset 
 |-  ( M e. A <-> E. i e. A i = M )
40 biorf 
 |-  ( -. E. i e. A i = M -> ( A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) <-> ( E. i e. A i = M \/ A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) )
41 39 40 sylnbi 
 |-  ( -. M e. A -> ( A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) <-> ( E. i e. A i = M \/ A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) )
42 41 adantl 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) <-> ( E. i e. A i = M \/ A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) )
43 orcom 
 |-  ( ( E. i e. A i = M \/ A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) <-> ( A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) \/ E. i e. A i = M ) )
44 42 43 bitrdi 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) <-> ( A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) \/ E. i e. A i = M ) ) )
45 38 44 syl5ibr 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. i e. A ( ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) \/ i = M ) -> A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
46 37 45 syl5bir 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) -> A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
47 olc 
 |-  ( ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) -> ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
48 47 ralimi 
 |-  ( A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) -> A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
49 46 48 impbid1 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) <-> A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
50 nfv 
 |-  F/ i ( B i^i C ) = (/)
51 nfcsb1v 
 |-  F/_ x [_ i / x ]_ B
52 nfcv 
 |-  F/_ x C
53 51 52 nfin 
 |-  F/_ x ( [_ i / x ]_ B i^i C )
54 53 nfeq1 
 |-  F/ x ( [_ i / x ]_ B i^i C ) = (/)
55 csbeq1a 
 |-  ( x = i -> B = [_ i / x ]_ B )
56 55 ineq1d 
 |-  ( x = i -> ( B i^i C ) = ( [_ i / x ]_ B i^i C ) )
57 56 eqeq1d 
 |-  ( x = i -> ( ( B i^i C ) = (/) <-> ( [_ i / x ]_ B i^i C ) = (/) ) )
58 50 54 57 cbvralw 
 |-  ( A. x e. A ( B i^i C ) = (/) <-> A. i e. A ( [_ i / x ]_ B i^i C ) = (/) )
59 58 a1i 
 |-  ( M e. V -> ( A. x e. A ( B i^i C ) = (/) <-> A. i e. A ( [_ i / x ]_ B i^i C ) = (/) ) )
60 ss0b 
 |-  ( U_ x e. A ( B i^i C ) C_ (/) <-> U_ x e. A ( B i^i C ) = (/) )
61 iunss 
 |-  ( U_ x e. A ( B i^i C ) C_ (/) <-> A. x e. A ( B i^i C ) C_ (/) )
62 iunin1 
 |-  U_ x e. A ( B i^i C ) = ( U_ x e. A B i^i C )
63 62 eqeq1i 
 |-  ( U_ x e. A ( B i^i C ) = (/) <-> ( U_ x e. A B i^i C ) = (/) )
64 60 61 63 3bitr3ri 
 |-  ( ( U_ x e. A B i^i C ) = (/) <-> A. x e. A ( B i^i C ) C_ (/) )
65 ss0b 
 |-  ( ( B i^i C ) C_ (/) <-> ( B i^i C ) = (/) )
66 65 ralbii 
 |-  ( A. x e. A ( B i^i C ) C_ (/) <-> A. x e. A ( B i^i C ) = (/) )
67 64 66 bitri 
 |-  ( ( U_ x e. A B i^i C ) = (/) <-> A. x e. A ( B i^i C ) = (/) )
68 67 a1i 
 |-  ( M e. V -> ( ( U_ x e. A B i^i C ) = (/) <-> A. x e. A ( B i^i C ) = (/) ) )
69 nfcvd 
 |-  ( M e. V -> F/_ x C )
70 69 1 csbiegf 
 |-  ( M e. V -> [_ M / x ]_ B = C )
71 70 ineq2d 
 |-  ( M e. V -> ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = ( [_ i / x ]_ B i^i C ) )
72 71 eqeq1d 
 |-  ( M e. V -> ( ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) <-> ( [_ i / x ]_ B i^i C ) = (/) ) )
73 72 ralbidv 
 |-  ( M e. V -> ( A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) <-> A. i e. A ( [_ i / x ]_ B i^i C ) = (/) ) )
74 59 68 73 3bitr4d 
 |-  ( M e. V -> ( ( U_ x e. A B i^i C ) = (/) <-> A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
75 74 adantr 
 |-  ( ( M e. V /\ -. M e. A ) -> ( ( U_ x e. A B i^i C ) = (/) <-> A. i e. A ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) )
76 49 75 bitr4d 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) <-> ( U_ x e. A B i^i C ) = (/) ) )
77 76 anbi2d 
 |-  ( ( M e. V /\ -. M e. A ) -> ( ( Disj_ x e. A B /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) <-> ( Disj_ x e. A B /\ ( U_ x e. A B i^i C ) = (/) ) ) )
78 orcom 
 |-  ( ( ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) \/ M = j ) <-> ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
79 78 ralbii 
 |-  ( A. j e. A ( ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) \/ M = j ) <-> A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
80 r19.30 
 |-  ( A. j e. A ( ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) \/ M = j ) -> ( A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) \/ E. j e. A M = j ) )
81 clel5 
 |-  ( M e. A <-> E. j e. A M = j )
82 biorf 
 |-  ( -. E. j e. A M = j -> ( A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> ( E. j e. A M = j \/ A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) )
83 81 82 sylnbi 
 |-  ( -. M e. A -> ( A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> ( E. j e. A M = j \/ A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) )
84 83 adantl 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> ( E. j e. A M = j \/ A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) )
85 orcom 
 |-  ( ( E. j e. A M = j \/ A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> ( A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) \/ E. j e. A M = j ) )
86 84 85 bitrdi 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> ( A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) \/ E. j e. A M = j ) ) )
87 80 86 syl5ibr 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. j e. A ( ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) \/ M = j ) -> A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
88 79 87 syl5bir 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) -> A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
89 olc 
 |-  ( ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) -> ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
90 89 ralimi 
 |-  ( A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) -> A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
91 88 90 impbid1 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
92 nfv 
 |-  F/ j ( B i^i C ) = (/)
93 nfcsb1v 
 |-  F/_ x [_ j / x ]_ B
94 93 52 nfin 
 |-  F/_ x ( [_ j / x ]_ B i^i C )
95 94 nfeq1 
 |-  F/ x ( [_ j / x ]_ B i^i C ) = (/)
96 csbeq1a 
 |-  ( x = j -> B = [_ j / x ]_ B )
97 96 ineq1d 
 |-  ( x = j -> ( B i^i C ) = ( [_ j / x ]_ B i^i C ) )
98 97 eqeq1d 
 |-  ( x = j -> ( ( B i^i C ) = (/) <-> ( [_ j / x ]_ B i^i C ) = (/) ) )
99 92 95 98 cbvralw 
 |-  ( A. x e. A ( B i^i C ) = (/) <-> A. j e. A ( [_ j / x ]_ B i^i C ) = (/) )
100 99 a1i 
 |-  ( M e. V -> ( A. x e. A ( B i^i C ) = (/) <-> A. j e. A ( [_ j / x ]_ B i^i C ) = (/) ) )
101 incom 
 |-  ( [_ j / x ]_ B i^i C ) = ( C i^i [_ j / x ]_ B )
102 101 eqeq1i 
 |-  ( ( [_ j / x ]_ B i^i C ) = (/) <-> ( C i^i [_ j / x ]_ B ) = (/) )
103 102 ralbii 
 |-  ( A. j e. A ( [_ j / x ]_ B i^i C ) = (/) <-> A. j e. A ( C i^i [_ j / x ]_ B ) = (/) )
104 100 103 bitrdi 
 |-  ( M e. V -> ( A. x e. A ( B i^i C ) = (/) <-> A. j e. A ( C i^i [_ j / x ]_ B ) = (/) ) )
105 70 ineq1d 
 |-  ( M e. V -> ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = ( C i^i [_ j / x ]_ B ) )
106 105 eqeq1d 
 |-  ( M e. V -> ( ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> ( C i^i [_ j / x ]_ B ) = (/) ) )
107 106 ralbidv 
 |-  ( M e. V -> ( A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> A. j e. A ( C i^i [_ j / x ]_ B ) = (/) ) )
108 104 68 107 3bitr4d 
 |-  ( M e. V -> ( ( U_ x e. A B i^i C ) = (/) <-> A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
109 108 adantr 
 |-  ( ( M e. V /\ -. M e. A ) -> ( ( U_ x e. A B i^i C ) = (/) <-> A. j e. A ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
110 91 109 bitr4d 
 |-  ( ( M e. V /\ -. M e. A ) -> ( A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) <-> ( U_ x e. A B i^i C ) = (/) ) )
111 77 110 anbi12d 
 |-  ( ( M e. V /\ -. M e. A ) -> ( ( ( Disj_ x e. A B /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) /\ A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) <-> ( ( Disj_ x e. A B /\ ( U_ x e. A B i^i C ) = (/) ) /\ ( U_ x e. A B i^i C ) = (/) ) ) )
112 anass 
 |-  ( ( ( Disj_ x e. A B /\ ( U_ x e. A B i^i C ) = (/) ) /\ ( U_ x e. A B i^i C ) = (/) ) <-> ( Disj_ x e. A B /\ ( ( U_ x e. A B i^i C ) = (/) /\ ( U_ x e. A B i^i C ) = (/) ) ) )
113 anidm 
 |-  ( ( ( U_ x e. A B i^i C ) = (/) /\ ( U_ x e. A B i^i C ) = (/) ) <-> ( U_ x e. A B i^i C ) = (/) )
114 113 anbi2i 
 |-  ( ( Disj_ x e. A B /\ ( ( U_ x e. A B i^i C ) = (/) /\ ( U_ x e. A B i^i C ) = (/) ) ) <-> ( Disj_ x e. A B /\ ( U_ x e. A B i^i C ) = (/) ) )
115 112 114 bitri 
 |-  ( ( ( Disj_ x e. A B /\ ( U_ x e. A B i^i C ) = (/) ) /\ ( U_ x e. A B i^i C ) = (/) ) <-> ( Disj_ x e. A B /\ ( U_ x e. A B i^i C ) = (/) ) )
116 111 115 bitrdi 
 |-  ( ( M e. V /\ -. M e. A ) -> ( ( ( Disj_ x e. A B /\ A. i e. A ( i = M \/ ( [_ i / x ]_ B i^i [_ M / x ]_ B ) = (/) ) ) /\ A. j e. A ( M = j \/ ( [_ M / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) <-> ( Disj_ x e. A B /\ ( U_ x e. A B i^i C ) = (/) ) ) )
117 35 116 bitrd 
 |-  ( ( M e. V /\ -. M e. A ) -> ( Disj_ x e. ( A u. { M } ) B <-> ( Disj_ x e. A B /\ ( U_ x e. A B i^i C ) = (/) ) ) )