Theorem disj1 4451

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.)

Assertion

Ref	Expression
disj1	⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem disj1

Step	Hyp	Ref	Expression
1		disj 4449	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵)
2		df-ral 3061	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
3	1, 2	bitri 275	1 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1537   = wceq 1539   ∈ wcel 2107  ∀wral 3060   ∩ cin 3949  ∅c0 4332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-dif 3953  df-in 3957  df-nul 4333

This theorem is referenced by:  reldisj  4452  disj3  4453  undif4  4466  disjsn  4710  funun  6611  zfregs2  9774  dfac5lem4  10167  dfac5lem4OLD  10169  isf32lem9  10402  fzodisj  13734  fzodisjsn  13738  inpr0  32551  bnj1280  35035  ecin0  38354  zfregs2VD  44866  dfac5prim  45012