Theorem bnj1541

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1541.1	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝐴 ≠ 𝐵 ) )
	bnj1541.2	⊢ ¬ 𝜑
Assertion	bnj1541	⊢ ( 𝜓 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		bnj1541.1	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝐴 ≠ 𝐵 ) )
2		bnj1541.2	⊢ ¬ 𝜑
3	2 1	mtbi	⊢ ¬ ( 𝜓 ∧ 𝐴 ≠ 𝐵 )
4	3	imnani	⊢ ( 𝜓 → ¬ 𝐴 ≠ 𝐵 )
5		nne	⊢ ( ¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵 )
6	4 5	sylib	⊢ ( 𝜓 → 𝐴 = 𝐵 )