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∩B=∅↔∀x∈A¬x∈B

Proof

Step Hyp Ref Expression
1 df-in ⊢A∩B=z|z∈A∧z∈B
2 1 eqeq1i ⊢A∩B=∅↔z|z∈A∧z∈B=∅
3 dfcleq ⊢∅=z|z∈A∧z∈B↔∀xx∈∅↔x∈z|z∈A∧z∈B
4 df-clab ⊢x∈z|z∈A∧z∈B↔xzz∈A∧z∈B
5 sb6 ⊢xzz∈A∧z∈B↔∀zz=x→z∈A∧z∈B
6 id ⊢z=x→z=x
7 eleq1w ⊢z=x→z∈A↔x∈A
8 7 biimpd ⊢z=x→z∈A→x∈A
9 eleq1w ⊢z=x→z∈B↔x∈B
10 9 biimpd ⊢z=x→z∈B→x∈B
11 8 10 anim12d ⊢z=x→z∈A∧z∈B→x∈A∧x∈B
12 6 11 embantd ⊢z=x→z=x→z∈A∧z∈B→x∈A∧x∈B
13 12 spimvw ⊢∀zz=x→z∈A∧z∈B→x∈A∧x∈B
14 eleq1a ⊢x∈A→z=x→z∈A
15 eleq1a ⊢x∈B→z=x→z∈B
16 14 15 anim12ii ⊢x∈A∧x∈B→z=x→z∈A∧z∈B
17 16 alrimiv ⊢x∈A∧x∈B→∀zz=x→z∈A∧z∈B
18 13 17 impbii ⊢∀zz=x→z∈A∧z∈B↔x∈A∧x∈B
19 4 5 18 3bitri ⊢x∈z|z∈A∧z∈B↔x∈A∧x∈B
20 19 bibi2i ⊢x∈∅↔x∈z|z∈A∧z∈B↔x∈∅↔x∈A∧x∈B
21 20 albii ⊢∀xx∈∅↔x∈z|z∈A∧z∈B↔∀xx∈∅↔x∈A∧x∈B
22 3 21 bitri ⊢∅=z|z∈A∧z∈B↔∀xx∈∅↔x∈A∧x∈B
23 eqcom ⊢z|z∈A∧z∈B=∅↔∅=z|z∈A∧z∈B
24 bicom ⊢x∈A∧x∈B↔x∈∅↔x∈∅↔x∈A∧x∈B
25 24 albii ⊢∀xx∈A∧x∈B↔x∈∅↔∀xx∈∅↔x∈A∧x∈B
26 22 23 25 3bitr4i ⊢z|z∈A∧z∈B=∅↔∀xx∈A∧x∈B↔x∈∅
27 imnan ⊢x∈A→¬x∈B↔¬x∈A∧x∈B
28 noel ⊢¬x∈∅
29 28 nbn ⊢¬x∈A∧x∈B↔x∈A∧x∈B↔x∈∅
30 27 29 bitr2i ⊢x∈A∧x∈B↔x∈∅↔x∈A→¬x∈B
31 30 albii ⊢∀xx∈A∧x∈B↔x∈∅↔∀xx∈A→¬x∈B
32 2 26 31 3bitri ⊢A∩B=∅↔∀xx∈A→¬x∈B
33 df-ral ⊢∀x∈A¬x∈B↔∀xx∈A→¬x∈B
34 32 33 bitr4i ⊢A∩B=∅↔∀x∈A¬x∈B