# Metamath Proof Explorer

## Theorem disj

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004) Avoid ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto, 28-Jun-2024)

Ref Expression
Assertion disj ${⊢}{A}\cap {B}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}$

### Proof

Step Hyp Ref Expression
1 df-in ${⊢}{A}\cap {B}=\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}$
2 1 eqeq1i ${⊢}{A}\cap {B}=\varnothing ↔\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}=\varnothing$
3 dfcleq ${⊢}\varnothing =\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \varnothing ↔{x}\in \left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}\right)$
4 df-clab ${⊢}{x}\in \left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}↔\left[{x}/{z}\right]\left({z}\in {A}\wedge {z}\in {B}\right)$
5 sb6 ${⊢}\left[{x}/{z}\right]\left({z}\in {A}\wedge {z}\in {B}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to \left({z}\in {A}\wedge {z}\in {B}\right)\right)$
6 id ${⊢}{z}={x}\to {z}={x}$
7 eleq1w ${⊢}{z}={x}\to \left({z}\in {A}↔{x}\in {A}\right)$
8 7 biimpd ${⊢}{z}={x}\to \left({z}\in {A}\to {x}\in {A}\right)$
9 eleq1w ${⊢}{z}={x}\to \left({z}\in {B}↔{x}\in {B}\right)$
10 9 biimpd ${⊢}{z}={x}\to \left({z}\in {B}\to {x}\in {B}\right)$
11 8 10 anim12d ${⊢}{z}={x}\to \left(\left({z}\in {A}\wedge {z}\in {B}\right)\to \left({x}\in {A}\wedge {x}\in {B}\right)\right)$
12 6 11 embantd ${⊢}{z}={x}\to \left(\left({z}={x}\to \left({z}\in {A}\wedge {z}\in {B}\right)\right)\to \left({x}\in {A}\wedge {x}\in {B}\right)\right)$
13 12 spimvw ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to \left({z}\in {A}\wedge {z}\in {B}\right)\right)\to \left({x}\in {A}\wedge {x}\in {B}\right)$
14 eleq1a ${⊢}{x}\in {A}\to \left({z}={x}\to {z}\in {A}\right)$
15 eleq1a ${⊢}{x}\in {B}\to \left({z}={x}\to {z}\in {B}\right)$
16 14 15 anim12ii ${⊢}\left({x}\in {A}\wedge {x}\in {B}\right)\to \left({z}={x}\to \left({z}\in {A}\wedge {z}\in {B}\right)\right)$
17 16 alrimiv ${⊢}\left({x}\in {A}\wedge {x}\in {B}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to \left({z}\in {A}\wedge {z}\in {B}\right)\right)$
18 13 17 impbii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to \left({z}\in {A}\wedge {z}\in {B}\right)\right)↔\left({x}\in {A}\wedge {x}\in {B}\right)$
19 4 5 18 3bitri ${⊢}{x}\in \left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}↔\left({x}\in {A}\wedge {x}\in {B}\right)$
20 19 bibi2i ${⊢}\left({x}\in \varnothing ↔{x}\in \left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}\right)↔\left({x}\in \varnothing ↔\left({x}\in {A}\wedge {x}\in {B}\right)\right)$
21 20 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \varnothing ↔{x}\in \left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \varnothing ↔\left({x}\in {A}\wedge {x}\in {B}\right)\right)$
22 3 21 bitri ${⊢}\varnothing =\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \varnothing ↔\left({x}\in {A}\wedge {x}\in {B}\right)\right)$
23 eqcom ${⊢}\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}=\varnothing ↔\varnothing =\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}$
24 bicom ${⊢}\left(\left({x}\in {A}\wedge {x}\in {B}\right)↔{x}\in \varnothing \right)↔\left({x}\in \varnothing ↔\left({x}\in {A}\wedge {x}\in {B}\right)\right)$
25 24 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {x}\in {B}\right)↔{x}\in \varnothing \right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \varnothing ↔\left({x}\in {A}\wedge {x}\in {B}\right)\right)$
26 22 23 25 3bitr4i ${⊢}\left\{{z}|\left({z}\in {A}\wedge {z}\in {B}\right)\right\}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {x}\in {B}\right)↔{x}\in \varnothing \right)$
27 imnan ${⊢}\left({x}\in {A}\to ¬{x}\in {B}\right)↔¬\left({x}\in {A}\wedge {x}\in {B}\right)$
28 noel ${⊢}¬{x}\in \varnothing$
29 28 nbn ${⊢}¬\left({x}\in {A}\wedge {x}\in {B}\right)↔\left(\left({x}\in {A}\wedge {x}\in {B}\right)↔{x}\in \varnothing \right)$
30 27 29 bitr2i ${⊢}\left(\left({x}\in {A}\wedge {x}\in {B}\right)↔{x}\in \varnothing \right)↔\left({x}\in {A}\to ¬{x}\in {B}\right)$
31 30 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\wedge {x}\in {B}\right)↔{x}\in \varnothing \right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{x}\in {B}\right)$
32 2 26 31 3bitri ${⊢}{A}\cap {B}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{x}\in {B}\right)$
33 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{x}\in {B}\right)$
34 32 33 bitr4i ${⊢}{A}\cap {B}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}\in {B}$