# 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 ${⊢}{x}={y}\to {A}={B}$
Assertion disjexc ${⊢}\left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\to {x}={y}\right)\to \left({A}={B}\vee {A}\cap {B}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 disjexc.1 ${⊢}{x}={y}\to {A}={B}$
2 1 imim2i ${⊢}\left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\to {x}={y}\right)\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\to {A}={B}\right)$
3 orcom ${⊢}\left({A}={B}\vee ¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\right)↔\left(¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\vee {A}={B}\right)$
4 df-in ${⊢}{A}\cap {B}=\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}$
5 4 neeq1i ${⊢}{A}\cap {B}\ne \varnothing ↔\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}\ne \varnothing$
6 abn0 ${⊢}\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}\ne \varnothing ↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)$
7 5 6 bitr2i ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)↔{A}\cap {B}\ne \varnothing$
8 7 necon2bbii ${⊢}{A}\cap {B}=\varnothing ↔¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)$
9 8 orbi2i ${⊢}\left({A}={B}\vee {A}\cap {B}=\varnothing \right)↔\left({A}={B}\vee ¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\right)$
10 imor ${⊢}\left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\to {A}={B}\right)↔\left(¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\vee {A}={B}\right)$
11 3 9 10 3bitr4i ${⊢}\left({A}={B}\vee {A}\cap {B}=\varnothing \right)↔\left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\to {A}={B}\right)$
12 2 11 sylibr ${⊢}\left(\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge {z}\in {B}\right)\to {x}={y}\right)\to \left({A}={B}\vee {A}\cap {B}=\varnothing \right)$