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

Metamath Proof Explorer

Theorem rexdifpr

Description: Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018) (Proof shortened by Wolf Lammen, 15-May-2025)

Ref Expression
Assertion rexdifpr ( ∃ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ) ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ∧ 𝜑 ) ) )
2 eldifpr ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) )
3 3anass ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ) )
4 2 3 bitri ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ) )
5 4 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ) ∧ 𝜑 ) )
6 df-3an ⊢ ( ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑 ) ↔ ( ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ∧ 𝜑 ) )
7 6 anbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ) ∧ 𝜑 ) ) )
8 1 5 7 3bitr4i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑 ) ) )
9 8 rexbii2 ⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 , 𝐶 } ) 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑥 ≠ 𝐵 ∧ 𝑥 ≠ 𝐶 ∧ 𝜑 ) )