Theorem disjif

Description: Property of a disjoint collection: if B ( x ) and B ( Y ) = D have a common element Z , then x = Y . (Contributed by Thierry Arnoux, 30-Dec-2016)

	Ref	Expression
Hypotheses	disjif.1	⊢ Ⅎ 𝑥 𝐶
	disjif.2	⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐶 )
Assertion	disjif	⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑥 = 𝑌 )

Proof

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 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑥 = 𝑌 )