Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-ru0 Structured version   Visualization version   GIF version

Theorem bj-ru0 31966
Description: The FOL part of Russell's paradox ru 3305 (see also bj-ru1 31967, bj-ru 31968). Use of elequ1 1945, bj-elequ12 31697, bj-spvv 31755 (instead of eleq1 2580, eleq12d 2586, spv 2151 as in ru 3305) permits to remove dependency on ax-10 1966, ax-11 1971, ax-12 1983, ax-13 2137, ax-ext 2494, df-sb 1831, df-clab 2501, df-cleq 2507, df-clel 2510. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
Assertion
Ref Expression
bj-ru0 ¬ ∀𝑥(𝑥𝑦 ↔ ¬ 𝑥𝑥)
Distinct variable group:   𝑥,𝑦

Proof of Theorem bj-ru0
StepHypRef Expression
1 pm5.19 373 . 2 ¬ (𝑦𝑦 ↔ ¬ 𝑦𝑦)
2 elequ1 1945 . . . 4 (𝑥 = 𝑦 → (𝑥𝑦𝑦𝑦))
3 bj-elequ12 31697 . . . . . 6 ((𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑥𝑦𝑦))
43anidms 674 . . . . 5 (𝑥 = 𝑦 → (𝑥𝑥𝑦𝑦))
54notbid 306 . . . 4 (𝑥 = 𝑦 → (¬ 𝑥𝑥 ↔ ¬ 𝑦𝑦))
62, 5bibi12d 333 . . 3 (𝑥 = 𝑦 → ((𝑥𝑦 ↔ ¬ 𝑥𝑥) ↔ (𝑦𝑦 ↔ ¬ 𝑦𝑦)))
76bj-spvv 31755 . 2 (∀𝑥(𝑥𝑦 ↔ ¬ 𝑥𝑥) → (𝑦𝑦 ↔ ¬ 𝑦𝑦))
81, 7mto 186 1 ¬ ∀𝑥(𝑥𝑦 ↔ ¬ 𝑥𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  bj-ru1  31967
  Copyright terms: Public domain W3C validator