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	|- ( E. x ( ph <-> -. ps ) <-> { x | ph } =/= { x | ps } )

Proof

Step	Hyp	Ref	Expression
1		df-ne	|- ( { x | ph } =/= { x | ps } <-> -. { x | ph } = { x | ps } )
2		exnal	|- ( E. x -. ( ph <-> ps ) <-> -. A. x ( ph <-> ps ) )
3		xor3	|- ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) )
4	3	exbii	|- ( E. x -. ( ph <-> ps ) <-> E. x ( ph <-> -. ps ) )
5	2 4	bitr3i	|- ( -. A. x ( ph <-> ps ) <-> E. x ( ph <-> -. ps ) )
6		abbi	|- ( A. x ( ph <-> ps ) <-> { x | ph } = { x | ps } )
7	5 6	xchnxbi	|- ( -. { x | ph } = { x | ps } <-> E. x ( ph <-> -. ps ) )
8	1 7	bitr2i	|- ( E. x ( ph <-> -. ps ) <-> { x | ph } =/= { x | ps } )