Definition df-xor 1510

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 1544) and the constant false ⊥ (df-fal 1554), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1586), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1587), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1588), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1589). Contrast with ∧ (df-an 397), ∨ (df-or 846), → (wi 4), and ⊼ (df-nan 1490). (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 1509	. 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  1511  xorcom  1512  xorcomOLD  1513  xorass  1514  excxor  1515  xor2  1516  xorneg2  1520  xorbi12i  1523  xorbi12iOLD  1524  xorbi12d  1525  anxordi  1526  xorexmid  1527  truxortru  1586  truxorfal  1587  falxorfal  1589  hadbi  1599  elsymdifxor  4214  sadadd2lem2  16341  f1omvdco3  19245  bj-bixor  35132  wl-df3xor2  36013  wl-3xorbi  36017  wl-2xor  36027  tsxo3  36671  tsxo4  36672  oneptri  41649  ifpxorxorb  41905  or3or  42417  axorbtnotaiffb  45258  axorbciffatcxorb  45260  aisbnaxb  45266  abnotbtaxb  45270  abnotataxb  45271  afv2orxorb  45580