Definition df-xor 1535

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 1566) and the constant false ⊥ (df-fal 1576), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1608), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1609), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1610), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1611). Contrast with ∧ (df-an 401), ∨ (df-or 861), → (wi 4), and ⊼ (df-nan 1515). (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 1534	. 2 wff (𝜑 ⊻ 𝜓)
4	1, 2	wb 209	. . 3 wff (𝜑 ↔ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ↔ 𝜓)
6	3, 5	wb 209	1 wff ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓))

This definition is referenced by:  xnor  1536  xorcom  1537  xorass  1538  excxor  1539  xor2  1540  xorneg2  1544  xorbi12i  1547  xorbi12d  1548  anxordi  1549  xorexmid  1550  truxortru  1608  truxorfal  1609  falxorfal  1611  hadbi  1621  elsymdifxor  4215  sadadd2lem2  16498  f1omvdco3  19510  bj-bixor  37046  wl-df3xor2  37975  wl-3xorbi  37979  wl-2xor  37989  tsxo3  38650  tsxo4  38651  oneptri  43846  ifpxorxorb  44099  or3or  44611  axorbtnotaiffb  47495  axorbciffatcxorb  47497  aisbnaxb  47503  abnotbtaxb  47507  abnotataxb  47508  afv2orxorb  47820