Theorem bnj1109

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

	Ref	Expression
Hypotheses	bnj1109.1	⊢ ∃ 𝑥 ( ( 𝐴 ≠ 𝐵 ∧ 𝜑 ) → 𝜓 )
	bnj1109.2	⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝜓 )
Assertion	bnj1109	⊢ ∃ 𝑥 ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		bnj1109.1	⊢ ∃ 𝑥 ( ( 𝐴 ≠ 𝐵 ∧ 𝜑 ) → 𝜓 )
2		bnj1109.2	⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝜓 )
3	2	ex	⊢ ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) )
4	3	a1i	⊢ ( ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) → ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) )
5	4	ax-gen	⊢ ∀ 𝑥 ( ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) → ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) )
6		impexp	⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝜑 ) → 𝜓 ) ↔ ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) )
7	6	exbii	⊢ ( ∃ 𝑥 ( ( 𝐴 ≠ 𝐵 ∧ 𝜑 ) → 𝜓 ) ↔ ∃ 𝑥 ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) )
8	1 7	mpbi	⊢ ∃ 𝑥 ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) )
9		exintr	⊢ ( ∀ 𝑥 ( ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) → ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) ) → ( ∃ 𝑥 ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) → ∃ 𝑥 ( ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) ∧ ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) ) ) )
10	5 8 9	mp2	⊢ ∃ 𝑥 ( ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) ∧ ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) )
11		exancom	⊢ ( ∃ 𝑥 ( ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) ∧ ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) ) ↔ ∃ 𝑥 ( ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) ∧ ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) ) )
12	10 11	mpbi	⊢ ∃ 𝑥 ( ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) ∧ ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) )
13		df-ne	⊢ ( 𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵 )
14	13	imbi1i	⊢ ( ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) ↔ ( ¬ 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) )
15		pm2.61	⊢ ( ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) → ( ( ¬ 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) ) )
16	15	imp	⊢ ( ( ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) ∧ ( ¬ 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) ) → ( 𝜑 → 𝜓 ) )
17	14 16	sylan2b	⊢ ( ( ( 𝐴 = 𝐵 → ( 𝜑 → 𝜓 ) ) ∧ ( 𝐴 ≠ 𝐵 → ( 𝜑 → 𝜓 ) ) ) → ( 𝜑 → 𝜓 ) )
18	12 17	bnj101	⊢ ∃ 𝑥 ( 𝜑 → 𝜓 )