Metamath Proof Explorer


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 ( ( ∃ 𝑧 ( 𝑧𝐴𝑧𝐵 ) → 𝑥 = 𝑦 ) → ( 𝐴 = 𝐵 ∨ ( 𝐴𝐵 ) = ∅ ) )