Theorem nabbi

Description: Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019) (Proof shortened by Wolf Lammen, 25-Nov-2019)

	Ref	Expression
Assertion	nabbi	$$⊢\exists x\left(\phi \leftrightarrow \neg \psi \right)\leftrightarrow \left\{x|\phi \right\}\ne \left\{x|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$$⊢\left\{x|\phi \right\}\ne \left\{x|\psi \right\}\leftrightarrow \neg \left\{x|\phi \right\}=\left\{x|\psi \right\}$$
2		exnal	$$⊢\exists x\neg \left(\phi \leftrightarrow \psi \right)\leftrightarrow \neg \forall x\left(\phi \leftrightarrow \psi \right)$$
3		xor3	$$⊢\neg \left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\phi \leftrightarrow \neg \psi \right)$$
4	3	exbii	$$⊢\exists x\neg \left(\phi \leftrightarrow \psi \right)\leftrightarrow \exists x\left(\phi \leftrightarrow \neg \psi \right)$$
5	2 4	bitr3i	$$⊢\neg \forall x\left(\phi \leftrightarrow \psi \right)\leftrightarrow \exists x\left(\phi \leftrightarrow \neg \psi \right)$$
6		abbi	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left\{x|\phi \right\}=\left\{x|\psi \right\}$$
7	5 6	xchnxbi	$$⊢\neg \left\{x|\phi \right\}=\left\{x|\psi \right\}\leftrightarrow \exists x\left(\phi \leftrightarrow \neg \psi \right)$$
8	1 7	bitr2i	$$⊢\exists x\left(\phi \leftrightarrow \neg \psi \right)\leftrightarrow \left\{x|\phi \right\}\ne \left\{x|\psi \right\}$$