Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjeq0 Structured version   Visualization version   GIF version

Theorem disjeq0 4166
 Description: Two disjoint sets are equal iff both are empty. (Contributed by AV, 19-Jun-2022.)
Assertion
Ref Expression
disjeq0 ((𝐴𝐵) = ∅ → (𝐴 = 𝐵 ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))

Proof of Theorem disjeq0
StepHypRef Expression
1 ineq1 3958 . . . . . 6 (𝐴 = 𝐵 → (𝐴𝐵) = (𝐵𝐵))
2 inidm 3971 . . . . . 6 (𝐵𝐵) = 𝐵
31, 2syl6eq 2821 . . . . 5 (𝐴 = 𝐵 → (𝐴𝐵) = 𝐵)
43eqeq1d 2773 . . . 4 (𝐴 = 𝐵 → ((𝐴𝐵) = ∅ ↔ 𝐵 = ∅))
5 eqtr 2790 . . . . . 6 ((𝐴 = 𝐵𝐵 = ∅) → 𝐴 = ∅)
6 simpr 471 . . . . . 6 ((𝐴 = 𝐵𝐵 = ∅) → 𝐵 = ∅)
75, 6jca 501 . . . . 5 ((𝐴 = 𝐵𝐵 = ∅) → (𝐴 = ∅ ∧ 𝐵 = ∅))
87ex 397 . . . 4 (𝐴 = 𝐵 → (𝐵 = ∅ → (𝐴 = ∅ ∧ 𝐵 = ∅)))
94, 8sylbid 230 . . 3 (𝐴 = 𝐵 → ((𝐴𝐵) = ∅ → (𝐴 = ∅ ∧ 𝐵 = ∅)))
109com12 32 . 2 ((𝐴𝐵) = ∅ → (𝐴 = 𝐵 → (𝐴 = ∅ ∧ 𝐵 = ∅)))
11 eqtr3 2792 . 2 ((𝐴 = ∅ ∧ 𝐵 = ∅) → 𝐴 = 𝐵)
1210, 11impbid1 215 1 ((𝐴𝐵) = ∅ → (𝐴 = 𝐵 ↔ (𝐴 = ∅ ∧ 𝐵 = ∅)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∩ cin 3722  ∅c0 4063 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730 This theorem is referenced by:  epnsym  8668
 Copyright terms: Public domain W3C validator