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	⊢ ( ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) ↔ { 𝑥 ∣ 𝜑 } ≠ { 𝑥 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		df-ne	⊢ ( { 𝑥 ∣ 𝜑 } ≠ { 𝑥 ∣ 𝜓 } ↔ ¬ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )
2		exnal	⊢ ( ∃ 𝑥 ¬ ( 𝜑 ↔ 𝜓 ) ↔ ¬ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )
3		xor3	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ↔ ¬ 𝜓 ) )
4	3	exbii	⊢ ( ∃ 𝑥 ¬ ( 𝜑 ↔ 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) )
5	2 4	bitr3i	⊢ ( ¬ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) )
6		abbi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )
7	5 6	xchnxbi	⊢ ( ¬ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) )
8	1 7	bitr2i	⊢ ( ∃ 𝑥 ( 𝜑 ↔ ¬ 𝜓 ) ↔ { 𝑥 ∣ 𝜑 } ≠ { 𝑥 ∣ 𝜓 } )