Definition df-xor 1503

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 1541) and the constant false ⊥ (df-fal 1551), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1583), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1584), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1585), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1586). Contrast with ∧ (df-an 400), ∨ (df-or 845), → (wi 4), and ⊼ (df-nan 1483). (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 1502	. 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  1504  xorcom  1505  xorcomOLD  1506  xorass  1507  excxor  1508  xor2  1509  xorneg2  1513  xorbi12i  1516  xorbi12iOLD  1517  xorbi12d  1518  anxordi  1519  xorexmid  1520  truxortru  1583  truxorfal  1584  falxorfal  1586  hadbi  1599  elsymdifxor  4176  sadadd2lem2  15789  f1omvdco3  18569  bj-bixor  34038  wl-df3xor2  34886  wl-3xorbi  34890  wl-2xor  34900  tsxo3  35577  tsxo4  35578  ifpxorxorb  40219  or3or  40724  axorbtnotaiffb  43496  axorbciffatcxorb  43498  aisbnaxb  43504  abnotbtaxb  43508  abnotataxb  43509  afv2orxorb  43784