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 ⊢ ( 𝑥 = 𝑀 → 𝐵 = 𝐶 )
Assertion disjunsn ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( Disj 𝑥 ∈ ( 𝐴 ∪ { 𝑀 } ) 𝐵 ↔ ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 disjunsn.s ⊢ ( 𝑥 = 𝑀 → 𝐵 = 𝐶 )
2 disjors ⊢ ( Disj 𝑥 ∈ ( 𝐴 ∪ { 𝑀 } ) 𝐵 ↔ ∀ 𝑖 ∈ ( 𝐴 ∪ { 𝑀 } ) ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
3 eqeq1 ⊢ ( 𝑖 = 𝑀 → ( 𝑖 = 𝑗 ↔ 𝑀 = 𝑗 ) )
4 csbeq1 ⊢ ( 𝑖 = 𝑀 → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 = ⦋ 𝑀 / 𝑥 ⦌ 𝐵 )
5 4 ineq1d ⊢ ( 𝑖 = 𝑀 → ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) )
6 5 eqeq1d ⊢ ( 𝑖 = 𝑀 → ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
7 3 6 orbi12d ⊢ ( 𝑖 = 𝑀 → ( ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
8 7 ralbidv ⊢ ( 𝑖 = 𝑀 → ( ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
9 8 ralunsn ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑖 ∈ ( 𝐴 ∪ { 𝑀 } ) ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ) )
10 2 9 bitrid ⊢ ( 𝑀 ∈ 𝑉 → ( Disj 𝑥 ∈ ( 𝐴 ∪ { 𝑀 } ) 𝐵 ↔ ( ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ) )
11 eqeq2 ⊢ ( 𝑗 = 𝑀 → ( 𝑖 = 𝑗 ↔ 𝑖 = 𝑀 ) )
12 csbeq1 ⊢ ( 𝑗 = 𝑀 → ⦋ 𝑗 / 𝑥 ⦌ 𝐵 = ⦋ 𝑀 / 𝑥 ⦌ 𝐵 )
13 12 ineq2d ⊢ ( 𝑗 = 𝑀 → ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) )
14 13 eqeq1d ⊢ ( 𝑗 = 𝑀 → ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
15 11 14 orbi12d ⊢ ( 𝑗 = 𝑀 → ( ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
16 15 ralunsn ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ) )
17 16 ralbidv ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ∀ 𝑖 ∈ 𝐴 ( ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ) )
18 eqeq2 ⊢ ( 𝑗 = 𝑀 → ( 𝑀 = 𝑗 ↔ 𝑀 = 𝑀 ) )
19 12 ineq2d ⊢ ( 𝑗 = 𝑀 → ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) )
20 19 eqeq1d ⊢ ( 𝑗 = 𝑀 → ( ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
21 18 20 orbi12d ⊢ ( 𝑗 = 𝑀 → ( ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( 𝑀 = 𝑀 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
22 21 ralunsn ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ( 𝑀 = 𝑀 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ) )
23 eqid ⊢ 𝑀 = 𝑀
24 23 orci ⊢ ( 𝑀 = 𝑀 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ )
25 24 biantru ⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ( 𝑀 = 𝑀 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
26 22 25 bitr4di ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
27 17 26 anbi12d ⊢ ( 𝑀 ∈ 𝑉 → ( ( ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ∀ 𝑗 ∈ ( 𝐴 ∪ { 𝑀 } ) ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ↔ ( ∀ 𝑖 ∈ 𝐴 ( ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ) )
28 10 27 bitrd ⊢ ( 𝑀 ∈ 𝑉 → ( Disj 𝑥 ∈ ( 𝐴 ∪ { 𝑀 } ) 𝐵 ↔ ( ∀ 𝑖 ∈ 𝐴 ( ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ) )
29 r19.26 ⊢ ( ∀ 𝑖 ∈ 𝐴 ( ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ↔ ( ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
30 disjors ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
31 30 anbi1i ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ↔ ( ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
32 29 31 bitr4i ⊢ ( ∀ 𝑖 ∈ 𝐴 ( ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ↔ ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
33 32 anbi1i ⊢ ( ( ∀ 𝑖 ∈ 𝐴 ( ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ∧ ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ↔ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
34 28 33 bitrdi ⊢ ( 𝑀 ∈ 𝑉 → ( Disj 𝑥 ∈ ( 𝐴 ∪ { 𝑀 } ) 𝐵 ↔ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ) )
35 34 adantr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( Disj 𝑥 ∈ ( 𝐴 ∪ { 𝑀 } ) 𝐵 ↔ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ) )
36 orcom ⊢ ( ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑖 = 𝑀 ) ↔ ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
37 36 ralbii ⊢ ( ∀ 𝑖 ∈ 𝐴 ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑖 = 𝑀 ) ↔ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
38 r19.30 ⊢ ( ∀ 𝑖 ∈ 𝐴 ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑖 = 𝑀 ) → ( ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ ∃ 𝑖 ∈ 𝐴 𝑖 = 𝑀 ) )
39 risset ⊢ ( 𝑀 ∈ 𝐴 ↔ ∃ 𝑖 ∈ 𝐴 𝑖 = 𝑀 )
40 biorf ⊢ ( ¬ ∃ 𝑖 ∈ 𝐴 𝑖 = 𝑀 → ( ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ∃ 𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
41 39 40 sylnbi ⊢ ( ¬ 𝑀 ∈ 𝐴 → ( ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ∃ 𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
42 41 adantl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ∃ 𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
43 orcom ⊢ ( ( ∃ 𝑖 ∈ 𝐴 𝑖 = 𝑀 ∨ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ ∃ 𝑖 ∈ 𝐴 𝑖 = 𝑀 ) )
44 42 43 bitrdi ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ ∃ 𝑖 ∈ 𝐴 𝑖 = 𝑀 ) ) )
45 38 44 imbitrrid ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑖 = 𝑀 ) → ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
46 37 45 biimtrrid ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
47 olc ⊢ ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ → ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
48 47 ralimi ⊢ ( ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ → ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
49 46 48 impbid1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
50 nfv ⊢ Ⅎ 𝑖 ( 𝐵 ∩ 𝐶 ) = ∅
51 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑖 / 𝑥 ⦌ 𝐵
52 nfcv ⊢ Ⅎ 𝑥 𝐶
53 51 52 nfin ⊢ Ⅎ 𝑥 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
54 53 nfeq1 ⊢ Ⅎ 𝑥 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅
55 csbeq1a ⊢ ( 𝑥 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑥 ⦌ 𝐵 )
56 55 ineq1d ⊢ ( 𝑥 = 𝑖 → ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
57 56 eqeq1d ⊢ ( 𝑥 = 𝑖 → ( ( 𝐵 ∩ 𝐶 ) = ∅ ↔ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ ) )
58 50 54 57 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ )
59 58 a1i ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ ) )
60 ss0b ⊢ ( ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ⊆ ∅ ↔ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ )
61 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ⊆ ∅ ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ⊆ ∅ )
62 iunin1 ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 )
63 62 eqeq1i ⊢ ( ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ )
64 60 61 63 3bitr3ri ⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ⊆ ∅ )
65 ss0b ⊢ ( ( 𝐵 ∩ 𝐶 ) ⊆ ∅ ↔ ( 𝐵 ∩ 𝐶 ) = ∅ )
66 65 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) ⊆ ∅ ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ )
67 64 66 bitri ⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ )
68 67 a1i ⊢ ( 𝑀 ∈ 𝑉 → ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ ) )
69 nfcvd ⊢ ( 𝑀 ∈ 𝑉 → Ⅎ 𝑥 𝐶 )
70 69 1 csbiegf ⊢ ( 𝑀 ∈ 𝑉 → ⦋ 𝑀 / 𝑥 ⦌ 𝐵 = 𝐶 )
71 70 ineq2d ⊢ ( 𝑀 ∈ 𝑉 → ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
72 71 eqeq1d ⊢ ( 𝑀 ∈ 𝑉 → ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ ) )
73 72 ralbidv ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ ) )
74 59 68 73 3bitr4d ⊢ ( 𝑀 ∈ 𝑉 → ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
75 74 adantr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑖 ∈ 𝐴 ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
76 49 75 bitr4d ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) )
77 76 anbi2d ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ↔ ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ) )
78 orcom ⊢ ( ( ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑀 = 𝑗 ) ↔ ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
79 78 ralbii ⊢ ( ∀ 𝑗 ∈ 𝐴 ( ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑀 = 𝑗 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
80 r19.30 ⊢ ( ∀ 𝑗 ∈ 𝐴 ( ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑀 = 𝑗 ) → ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ ∃ 𝑗 ∈ 𝐴 𝑀 = 𝑗 ) )
81 clel5 ⊢ ( 𝑀 ∈ 𝐴 ↔ ∃ 𝑗 ∈ 𝐴 𝑀 = 𝑗 )
82 biorf ⊢ ( ¬ ∃ 𝑗 ∈ 𝐴 𝑀 = 𝑗 → ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ∃ 𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
83 81 82 sylnbi ⊢ ( ¬ 𝑀 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ∃ 𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
84 83 adantl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ∃ 𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) )
85 orcom ⊢ ( ( ∃ 𝑗 ∈ 𝐴 𝑀 = 𝑗 ∨ ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ ∃ 𝑗 ∈ 𝐴 𝑀 = 𝑗 ) )
86 84 85 bitrdi ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ ∃ 𝑗 ∈ 𝐴 𝑀 = 𝑗 ) ) )
87 80 86 imbitrrid ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑗 ∈ 𝐴 ( ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ∨ 𝑀 = 𝑗 ) → ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
88 79 87 biimtrrid ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
89 olc ⊢ ( ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ → ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
90 89 ralimi ⊢ ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ → ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
91 88 90 impbid1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
92 nfv ⊢ Ⅎ 𝑗 ( 𝐵 ∩ 𝐶 ) = ∅
93 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑗 / 𝑥 ⦌ 𝐵
94 93 52 nfin ⊢ Ⅎ 𝑥 ( ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ∩ 𝐶 )
95 94 nfeq1 ⊢ Ⅎ 𝑥 ( ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅
96 csbeq1a ⊢ ( 𝑥 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑥 ⦌ 𝐵 )
97 96 ineq1d ⊢ ( 𝑥 = 𝑗 → ( 𝐵 ∩ 𝐶 ) = ( ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) )
98 97 eqeq1d ⊢ ( 𝑥 = 𝑗 → ( ( 𝐵 ∩ 𝐶 ) = ∅ ↔ ( ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ ) )
99 92 95 98 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ )
100 99 a1i ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ ) )
101 incom ⊢ ( ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ( 𝐶 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 )
102 101 eqeq1i ⊢ ( ( ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ ↔ ( 𝐶 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ )
103 102 ralbii ⊢ ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑗 ∈ 𝐴 ( 𝐶 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ )
104 100 103 bitrdi ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑗 ∈ 𝐴 ( 𝐶 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
105 70 ineq1d ⊢ ( 𝑀 ∈ 𝑉 → ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ( 𝐶 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) )
106 105 eqeq1d ⊢ ( 𝑀 ∈ 𝑉 → ( ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ( 𝐶 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
107 106 ralbidv ⊢ ( 𝑀 ∈ 𝑉 → ( ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ∀ 𝑗 ∈ 𝐴 ( 𝐶 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
108 104 68 107 3bitr4d ⊢ ( 𝑀 ∈ 𝑉 → ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
109 108 adantr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ↔ ∀ 𝑗 ∈ 𝐴 ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
110 91 109 bitr4d ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) )
111 77 110 anbi12d ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ↔ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ) )
112 anass ⊢ ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ) )
113 anidm ⊢ ( ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ )
114 113 anbi2i ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ) ↔ ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) )
115 112 114 bitri ⊢ ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ↔ ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) )
116 111 115 bitrdi ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝑖 = 𝑀 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ∧ ∀ 𝑗 ∈ 𝐴 ( 𝑀 = 𝑗 ∨ ( ⦋ 𝑀 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) ↔ ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ) )
117 35 116 bitrd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ¬ 𝑀 ∈ 𝐴 ) → ( Disj 𝑥 ∈ ( 𝐴 ∪ { 𝑀 } ) 𝐵 ↔ ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝐶 ) = ∅ ) ) )