This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∃ x A ≠ B ∧ φ → ψ
bnj1109.2 ⊢ A = B ∧ φ → ψ
Assertion bnj1109 ⊢ ∃ x φ → ψ

Proof

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