Theorem raldifsnb

Description: Restricted universal quantification on a class difference with a singleton in terms of an implication. (Contributed by Alexander van der Vekens, 26-Jan-2018)

	Ref	Expression
Assertion	raldifsnb	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ 𝑌 → 𝜑 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 𝑌 } ) 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		velsn	⊢ ( 𝑥 ∈ { 𝑌 } ↔ 𝑥 = 𝑌 )
2		nnel	⊢ ( ¬ 𝑥 ∉ { 𝑌 } ↔ 𝑥 ∈ { 𝑌 } )
3		nne	⊢ ( ¬ 𝑥 ≠ 𝑌 ↔ 𝑥 = 𝑌 )
4	1 2 3	3bitr4ri	⊢ ( ¬ 𝑥 ≠ 𝑌 ↔ ¬ 𝑥 ∉ { 𝑌 } )
5	4	con4bii	⊢ ( 𝑥 ≠ 𝑌 ↔ 𝑥 ∉ { 𝑌 } )
6	5	imbi1i	⊢ ( ( 𝑥 ≠ 𝑌 → 𝜑 ) ↔ ( 𝑥 ∉ { 𝑌 } → 𝜑 ) )
7	6	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ 𝑌 → 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∉ { 𝑌 } → 𝜑 ) )
8		raldifb	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∉ { 𝑌 } → 𝜑 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 𝑌 } ) 𝜑 )
9	7 8	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ 𝑌 → 𝜑 ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 𝑌 } ) 𝜑 )