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 ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ¬ 𝜑 ) → ∃ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) 𝜑 )

Proof

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