Definition df-xor 1511

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 1545) and the constant false ⊥ (df-fal 1555), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1587), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1588), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1589), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1590). Contrast with ∧ (df-an 398), ∨ (df-or 847), → (wi 4), and ⊼ (df-nan 1491). (Contributed by FL, 22-Nov-2010.)

Assertion

Ref	Expression
df-xor	⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

Detailed syntax breakdown of Definition df-xor

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3	1, 2	wxo 1510	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 205	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1512  xorcom  1513  xorcomOLD  1514  xorass  1515  excxor  1516  xor2  1517  xorneg2  1521  xorbi12i  1524  xorbi12iOLD  1525  xorbi12d  1526  anxordi  1527  xorexmid  1528  truxortru  1587  truxorfal  1588  falxorfal  1590  hadbi  1600  elsymdifxor  4250  sadadd2lem2  16391  f1omvdco3  19317  bj-bixor  35517  wl-df3xor2  36398  wl-3xorbi  36402  wl-2xor  36412  tsxo3  37055  tsxo4  37056  oneptri  42054  ifpxorxorb  42310  or3or  42822  axorbtnotaiffb  45661  axorbciffatcxorb  45663  aisbnaxb  45669  abnotbtaxb  45673  abnotataxb  45674  afv2orxorb  45984