:: deftheorem Def9 defines 'eqv' BVFUNC_1:def 9 :
for A being non empty set
for p, q, b₄ being Function of A,BOOLEAN holds
( b₄ = p 'eqv' q iff for x being Element of A holds b₄ . x = 'not' ((p . x) 'xor' (q . x)) );