Step |
Hyp |
Ref |
Expression |
1 |
|
disjif.1 |
⊢ Ⅎ 𝑥 𝐶 |
2 |
|
disjif.2 |
⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐶 ) |
3 |
|
inelcm |
⊢ ( ( 𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) |
4 |
1 2
|
disji2f |
⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑌 ) → ( 𝐵 ∩ 𝐶 ) = ∅ ) |
5 |
4
|
3expia |
⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( 𝑥 ≠ 𝑌 → ( 𝐵 ∩ 𝐶 ) = ∅ ) ) |
6 |
5
|
necon1d |
⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ) → ( ( 𝐵 ∩ 𝐶 ) ≠ ∅ → 𝑥 = 𝑌 ) ) |
7 |
6
|
3impia |
⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) → 𝑥 = 𝑌 ) |
8 |
3 7
|
syl3an3 |
⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑥 = 𝑌 ) |