New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-xor GIF version

Definition df-xor 1305
 Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. After we define the constant true ⊤ (df-tru 1319) and the constant false ⊥ (df-fal 1320), we will be able to prove these truth table values: (( ⊤ ⊻ ⊤ ) ↔ ⊥ ) (truxortru 1358), (( ⊤ ⊻ ⊥ ) ↔ ⊤ ) (truxorfal 1359), (( ⊥ ⊻ ⊤ ) ↔ ⊤ ) (falxortru 1360), and (( ⊥ ⊻ ⊥ ) ↔ ⊥ ) (falxorfal 1361). Contrast with ∧ (df-an 360), ∨ (df-or 359), → (wi 4), and ⊼ (df-nan 1288) . (Contributed by FL, 22-Nov-2010.)
Assertion
Ref Expression
df-xor ((φψ) ↔ ¬ (φψ))

Detailed syntax breakdown of Definition df-xor
StepHypRef Expression
1 wph . . 3 wff φ
2 wps . . 3 wff ψ
31, 2wxo 1304 . 2 wff (φψ)
41, 2wb 176 . . 3 wff (φψ)
54wn 3 . 2 wff ¬ (φψ)
63, 5wb 176 1 wff ((φψ) ↔ ¬ (φψ))
 Colors of variables: wff setvar class This definition is referenced by:  xnor  1306  xorcom  1307  xorass  1308  excxor  1309  xor2  1310  xorneg1  1311  xorbi12i  1314  xorbi12d  1315  truxortru  1358  truxorfal  1359  falxortru  1360  falxorfal  1361  hadbi  1387  had0  1403  mpto2  1534  mpto2OLD  1535  mtp-xorOLD  1537
 Copyright terms: Public domain W3C validator