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

Metamath Proof Explorer

Theorem rexdifi

Description: Restricted existential quantification over a difference. (Contributed by AV, 25-Oct-2023)

Ref Expression
Assertion rexdifi ⊢ ∃ x ∈ A φ ∧ ∀ x ∈ B ¬ φ → ∃ x ∈ A ∖ B φ

Proof

Step Hyp Ref Expression
1 df-rex ⊢ ∃ x ∈ A φ ↔ ∃ x x ∈ A ∧ φ
2 df-ral ⊢ ∀ x ∈ B ¬ φ ↔ ∀ x x ∈ B → ¬ φ
3 nfa1 ⊢ Ⅎ x ∀ x x ∈ B → ¬ φ
4 simprl ⊢ ∀ x x ∈ B → ¬ φ ∧ x ∈ A ∧ φ → x ∈ A
5 con2 ⊢ x ∈ B → ¬ φ → φ → ¬ x ∈ B
6 5 sps ⊢ ∀ x x ∈ B → ¬ φ → φ → ¬ x ∈ B
7 6 com12 ⊢ φ → ∀ x x ∈ B → ¬ φ → ¬ x ∈ B
8 7 adantl ⊢ x ∈ A ∧ φ → ∀ x x ∈ B → ¬ φ → ¬ x ∈ B
9 8 impcom ⊢ ∀ x x ∈ B → ¬ φ ∧ x ∈ A ∧ φ → ¬ x ∈ B
10 4 9 eldifd ⊢ ∀ x x ∈ B → ¬ φ ∧ x ∈ A ∧ φ → x ∈ A ∖ B
11 simprr ⊢ ∀ x x ∈ B → ¬ φ ∧ x ∈ A ∧ φ → φ
12 10 11 jca ⊢ ∀ x x ∈ B → ¬ φ ∧ x ∈ A ∧ φ → x ∈ A ∖ B ∧ φ
13 12 ex ⊢ ∀ x x ∈ B → ¬ φ → x ∈ A ∧ φ → x ∈ A ∖ B ∧ φ
14 3 13 eximd ⊢ ∀ x x ∈ B → ¬ φ → ∃ x x ∈ A ∧ φ → ∃ x x ∈ A ∖ B ∧ φ
15 14 impcom ⊢ ∃ x x ∈ A ∧ φ ∧ ∀ x x ∈ B → ¬ φ → ∃ x x ∈ A ∖ B ∧ φ
16 1 2 15 syl2anb ⊢ ∃ x ∈ A φ ∧ ∀ x ∈ B ¬ φ → ∃ x x ∈ A ∖ B ∧ φ
17 df-rex ⊢ ∃ x ∈ A ∖ B φ ↔ ∃ x x ∈ A ∖ B ∧ φ
18 16 17 sylibr ⊢ ∃ x ∈ A φ ∧ ∀ x ∈ B ¬ φ → ∃ x ∈ A ∖ B φ