Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-nfeqfb Structured version   Visualization version   GIF version

Theorem wl-nfeqfb 37233
Description: Extend nfeqf 2375 to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019.)
Assertion
Ref Expression
wl-nfeqfb (Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))

Proof of Theorem wl-nfeqfb
StepHypRef Expression
1 nf5r 2183 . . . . 5 (Ⅎ𝑥 𝑦 = 𝑧 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
21imp 405 . . . 4 ((Ⅎ𝑥 𝑦 = 𝑧𝑦 = 𝑧) → ∀𝑥 𝑦 = 𝑧)
3 wl-aleq 37232 . . . . 5 (∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)))
43simprbi 495 . . . 4 (∀𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
52, 4syl 17 . . 3 ((Ⅎ𝑥 𝑦 = 𝑧𝑦 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
6 nfnt 1852 . . . . . 6 (Ⅎ𝑥 𝑦 = 𝑧 → Ⅎ𝑥 ¬ 𝑦 = 𝑧)
76nf5rd 2185 . . . . 5 (Ⅎ𝑥 𝑦 = 𝑧 → (¬ 𝑦 = 𝑧 → ∀𝑥 ¬ 𝑦 = 𝑧))
87imp 405 . . . 4 ((Ⅎ𝑥 𝑦 = 𝑧 ∧ ¬ 𝑦 = 𝑧) → ∀𝑥 ¬ 𝑦 = 𝑧)
9 alnex 1776 . . . . . 6 (∀𝑥 ¬ 𝑦 = 𝑧 ↔ ¬ ∃𝑥 𝑦 = 𝑧)
10 wl-exeq 37231 . . . . . 6 (∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧))
119, 10xchbinx 333 . . . . 5 (∀𝑥 ¬ 𝑦 = 𝑧 ↔ ¬ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧))
12 3ioran 1103 . . . . 5 (¬ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧) ↔ (¬ 𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧))
1311, 12sylbb 218 . . . 4 (∀𝑥 ¬ 𝑦 = 𝑧 → (¬ 𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧))
14 3simpc 1147 . . . 4 ((¬ 𝑦 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧))
15 pm5.21 823 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
168, 13, 14, 154syl 19 . . 3 ((Ⅎ𝑥 𝑦 = 𝑧 ∧ ¬ 𝑦 = 𝑧) → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
175, 16pm2.61dan 811 . 2 (Ⅎ𝑥 𝑦 = 𝑧 → (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
18 ax7 2012 . . . . 5 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
1918al2imi 1810 . . . 4 (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
20 nftht 1787 . . . 4 (∀𝑥 𝑦 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧)
2119, 20syl6 35 . . 3 (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧))
22 nfeqf 2375 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 = 𝑧)
2322ex 411 . . 3 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑦 = 𝑧))
2421, 23bija 379 . 2 ((∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑦 = 𝑧)
2517, 24impbii 208 1 (Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 394  w3o 1083  w3a 1084  wal 1532  wex 1774  wnf 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-10 2130  ax-12 2167  ax-13 2366
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-ex 1775  df-nf 1779
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator