Theorem disjexc

Description: A variant of disjex , applicable for more generic families. (Contributed by Thierry Arnoux, 4-Oct-2016)

	Ref	Expression
Hypothesis	disjexc.1	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
Assertion	disjexc	⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝑥 = 𝑦 ) → ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		disjexc.1	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
2	1	imim2i	⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝑥 = 𝑦 ) → ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 = 𝐵 ) )
3		orcom	⊢ ( ( 𝐴 = 𝐵 ∨ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ↔ ( ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∨ 𝐴 = 𝐵 ) )
4		df-in	⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) }
5	4	neeq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ ∅ ↔ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ≠ ∅ )
6		abn0	⊢ ( { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) } ≠ ∅ ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
7	5 6	bitr2i	⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
8	7	necon2bbii	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
9	8	orbi2i	⊢ ( ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) ↔ ( 𝐴 = 𝐵 ∨ ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) )
10		imor	⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 = 𝐵 ) ↔ ( ¬ ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ∨ 𝐴 = 𝐵 ) )
11	3 9 10	3bitr4i	⊢ ( ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) ↔ ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝐴 = 𝐵 ) )
12	2 11	sylibr	⊢ ( ( ∃ 𝑧 ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → 𝑥 = 𝑦 ) → ( 𝐴 = 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = ∅ ) )