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

Theorem disj 4408
Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) Avoid ax-10 2138, ax-11 2155, ax-12 2172. (Revised by Gino Giotto, 28-Jun-2024.)
Assertion
Ref Expression
disj ((𝐴𝐵) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem disj
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-in 3918 . . . 4 (𝐴𝐵) = {𝑧 ∣ (𝑧𝐴𝑧𝐵)}
21eqeq1i 2738 . . 3 ((𝐴𝐵) = ∅ ↔ {𝑧 ∣ (𝑧𝐴𝑧𝐵)} = ∅)
3 dfcleq 2726 . . . . 5 (∅ = {𝑧 ∣ (𝑧𝐴𝑧𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)}))
4 df-clab 2711 . . . . . . . 8 (𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)} ↔ [𝑥 / 𝑧](𝑧𝐴𝑧𝐵))
5 sb6 2089 . . . . . . . 8 ([𝑥 / 𝑧](𝑧𝐴𝑧𝐵) ↔ ∀𝑧(𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)))
6 id 22 . . . . . . . . . . 11 (𝑧 = 𝑥𝑧 = 𝑥)
7 eleq1w 2817 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
87biimpd 228 . . . . . . . . . . . 12 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
9 eleq1w 2817 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (𝑧𝐵𝑥𝐵))
109biimpd 228 . . . . . . . . . . . 12 (𝑧 = 𝑥 → (𝑧𝐵𝑥𝐵))
118, 10anim12d 610 . . . . . . . . . . 11 (𝑧 = 𝑥 → ((𝑧𝐴𝑧𝐵) → (𝑥𝐴𝑥𝐵)))
126, 11embantd 59 . . . . . . . . . 10 (𝑧 = 𝑥 → ((𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)) → (𝑥𝐴𝑥𝐵)))
1312spimvw 2000 . . . . . . . . 9 (∀𝑧(𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)) → (𝑥𝐴𝑥𝐵))
14 eleq1a 2829 . . . . . . . . . . 11 (𝑥𝐴 → (𝑧 = 𝑥𝑧𝐴))
15 eleq1a 2829 . . . . . . . . . . 11 (𝑥𝐵 → (𝑧 = 𝑥𝑧𝐵))
1614, 15anim12ii 619 . . . . . . . . . 10 ((𝑥𝐴𝑥𝐵) → (𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)))
1716alrimiv 1931 . . . . . . . . 9 ((𝑥𝐴𝑥𝐵) → ∀𝑧(𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)))
1813, 17impbii 208 . . . . . . . 8 (∀𝑧(𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)) ↔ (𝑥𝐴𝑥𝐵))
194, 5, 183bitri 297 . . . . . . 7 (𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)} ↔ (𝑥𝐴𝑥𝐵))
2019bibi2i 338 . . . . . 6 ((𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)}) ↔ (𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
2120albii 1822 . . . . 5 (∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)}) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
223, 21bitri 275 . . . 4 (∅ = {𝑧 ∣ (𝑧𝐴𝑧𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
23 eqcom 2740 . . . 4 ({𝑧 ∣ (𝑧𝐴𝑧𝐵)} = ∅ ↔ ∅ = {𝑧 ∣ (𝑧𝐴𝑧𝐵)})
24 bicom 221 . . . . 5 (((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
2524albii 1822 . . . 4 (∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
2622, 23, 253bitr4i 303 . . 3 ({𝑧 ∣ (𝑧𝐴𝑧𝐵)} = ∅ ↔ ∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅))
27 imnan 401 . . . . 5 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ ¬ (𝑥𝐴𝑥𝐵))
28 noel 4291 . . . . . 6 ¬ 𝑥 ∈ ∅
2928nbn 373 . . . . 5 (¬ (𝑥𝐴𝑥𝐵) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅))
3027, 29bitr2i 276 . . . 4 (((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥𝐴 → ¬ 𝑥𝐵))
3130albii 1822 . . 3 (∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
322, 26, 313bitri 297 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
33 df-ral 3062 . 2 (∀𝑥𝐴 ¬ 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
3432, 33bitr4i 278 1 ((𝐴𝐵) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  [wsb 2068  wcel 2107  {cab 2710  wral 3061  cin 3910  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-dif 3914  df-in 3918  df-nul 4284
This theorem is referenced by:  disjr  4410  disj1  4411  disjne  4415  disjord  5094  disjiund  5096  otiunsndisj  5478  dfpo2  6249  onxpdisj  6444  f0rn0  6728  onint  7726  zfreg  9536  kmlem4  10094  fin23lem30  10283  fin23lem31  10284  isf32lem3  10296  fpwwe2  10584  renfdisj  11220  fvinim0ffz  13697  s3iunsndisj  14859  metdsge  24228  ssltdisj  27182  2wspmdisj  29323  subfacp1lem1  33830  dvmptfprodlem  44271  stoweidlem26  44353  stoweidlem59  44386  iundjiunlem  44786  otiunsndisjX  45597
  Copyright terms: Public domain W3C validator