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

Theorem disj 4345
 Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) Avoid ax-10 2143, ax-11 2159, ax-12 2176. (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 3866 . . . 4 (𝐴𝐵) = {𝑧 ∣ (𝑧𝐴𝑧𝐵)}
21eqeq1i 2764 . . 3 ((𝐴𝐵) = ∅ ↔ {𝑧 ∣ (𝑧𝐴𝑧𝐵)} = ∅)
3 dfcleq 2752 . . . . 5 (∅ = {𝑧 ∣ (𝑧𝐴𝑧𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)}))
4 df-clab 2737 . . . . . . . 8 (𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)} ↔ [𝑥 / 𝑧](𝑧𝐴𝑧𝐵))
5 sb6 2091 . . . . . . . 8 ([𝑥 / 𝑧](𝑧𝐴𝑧𝐵) ↔ ∀𝑧(𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)))
6 id 22 . . . . . . . . . . 11 (𝑧 = 𝑥𝑧 = 𝑥)
7 eleq1w 2835 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
87biimpd 232 . . . . . . . . . . . 12 (𝑧 = 𝑥 → (𝑧𝐴𝑥𝐴))
9 eleq1w 2835 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (𝑧𝐵𝑥𝐵))
109biimpd 232 . . . . . . . . . . . 12 (𝑧 = 𝑥 → (𝑧𝐵𝑥𝐵))
118, 10anim12d 612 . . . . . . . . . . 11 (𝑧 = 𝑥 → ((𝑧𝐴𝑧𝐵) → (𝑥𝐴𝑥𝐵)))
126, 11embantd 59 . . . . . . . . . 10 (𝑧 = 𝑥 → ((𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)) → (𝑥𝐴𝑥𝐵)))
1312spimvw 2003 . . . . . . . . 9 (∀𝑧(𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)) → (𝑥𝐴𝑥𝐵))
14 eleq1a 2848 . . . . . . . . . . 11 (𝑥𝐴 → (𝑧 = 𝑥𝑧𝐴))
15 eleq1a 2848 . . . . . . . . . . 11 (𝑥𝐵 → (𝑧 = 𝑥𝑧𝐵))
1614, 15anim12ii 621 . . . . . . . . . 10 ((𝑥𝐴𝑥𝐵) → (𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)))
1716alrimiv 1929 . . . . . . . . 9 ((𝑥𝐴𝑥𝐵) → ∀𝑧(𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)))
1813, 17impbii 212 . . . . . . . 8 (∀𝑧(𝑧 = 𝑥 → (𝑧𝐴𝑧𝐵)) ↔ (𝑥𝐴𝑥𝐵))
194, 5, 183bitri 301 . . . . . . 7 (𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)} ↔ (𝑥𝐴𝑥𝐵))
2019bibi2i 342 . . . . . 6 ((𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)}) ↔ (𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
2120albii 1822 . . . . 5 (∀𝑥(𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑧 ∣ (𝑧𝐴𝑧𝐵)}) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
223, 21bitri 278 . . . 4 (∅ = {𝑧 ∣ (𝑧𝐴𝑧𝐵)} ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
23 eqcom 2766 . . . 4 ({𝑧 ∣ (𝑧𝐴𝑧𝐵)} = ∅ ↔ ∅ = {𝑧 ∣ (𝑧𝐴𝑧𝐵)})
24 bicom 225 . . . . 5 (((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
2524albii 1822 . . . 4 (∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥𝐵)))
2622, 23, 253bitr4i 307 . . 3 ({𝑧 ∣ (𝑧𝐴𝑧𝐵)} = ∅ ↔ ∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅))
27 imnan 404 . . . . 5 ((𝑥𝐴 → ¬ 𝑥𝐵) ↔ ¬ (𝑥𝐴𝑥𝐵))
28 noel 4231 . . . . . 6 ¬ 𝑥 ∈ ∅
2928nbn 377 . . . . 5 (¬ (𝑥𝐴𝑥𝐵) ↔ ((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅))
3027, 29bitr2i 279 . . . 4 (((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ (𝑥𝐴 → ¬ 𝑥𝐵))
3130albii 1822 . . 3 (∀𝑥((𝑥𝐴𝑥𝐵) ↔ 𝑥 ∈ ∅) ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
322, 26, 313bitri 301 . 2 ((𝐴𝐵) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
33 df-ral 3076 . 2 (∀𝑥𝐴 ¬ 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥𝐵))
3432, 33bitr4i 281 1 ((𝐴𝐵) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1537   = wceq 1539  [wsb 2070   ∈ wcel 2112  {cab 2736  ∀wral 3071   ∩ cin 3858  ∅c0 4226 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-ral 3076  df-dif 3862  df-in 3866  df-nul 4227 This theorem is referenced by:  disjr  4347  disj1  4348  disjne  4352  disjord  5021  disjiund  5023  otiunsndisj  5380  onxpdisj  6290  f0rn0  6550  onint  7510  zfreg  9085  kmlem4  9606  fin23lem30  9795  fin23lem31  9796  isf32lem3  9808  fpwwe2  10096  renfdisj  10732  fvinim0ffz  13198  s3iunsndisj  14368  metdsge  23543  2wspmdisj  28214  subfacp1lem1  32650  dfpo2  33231  dvmptfprodlem  42945  stoweidlem26  43027  stoweidlem59  43060  iundjiunlem  43457  otiunsndisjX  44196
 Copyright terms: Public domain W3C validator