Theorem nabbib

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) Definitial form. (Revised by Wolf Lammen, 5-Mar-2025)

	Ref	Expression
Assertion	nabbib	$$⊢\left\{x|\phi \right\}\ne \left\{x|\psi \right\}\leftrightarrow \exists x\left(\phi \leftrightarrow \neg \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		abbib	$$⊢\left\{x|\phi \right\}=\left\{x|\psi \right\}\leftrightarrow \forall x\left(\phi \leftrightarrow \psi \right)$$
7	5 6	xchnxbir	$$⊢\neg \left\{x|\phi \right\}=\left\{x|\psi \right\}\leftrightarrow \exists x\left(\phi \leftrightarrow \neg \psi \right)$$
8	1 7	bitri	$$⊢\left\{x|\phi \right\}\ne \left\{x|\psi \right\}\leftrightarrow \exists x\left(\phi \leftrightarrow \neg \psi \right)$$