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 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1584), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1585), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1586), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1587). Contrast with ∧ (df-an 396), ∨ (df-or 848), → (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 206	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 206	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1512  xorcom  1513  xorass  1514  excxor  1515  xor2  1516  xorneg2  1520  xorbi12i  1523  xorbi12d  1524  anxordi  1525  xorexmid  1526  truxortru  1584  truxorfal  1585  falxorfal  1587  hadbi  1597  elsymdifxor  4259  sadadd2lem2  16488  f1omvdco3  19468  bj-bixor  36593  wl-df3xor2  37471  wl-3xorbi  37475  wl-2xor  37485  tsxo3  38147  tsxo4  38148  oneptri  43274  ifpxorxorb  43529  or3or  44041  axorbtnotaiffb  46920  axorbciffatcxorb  46922  aisbnaxb  46928  abnotbtaxb  46932  abnotataxb  46933  afv2orxorb  47245