Theorem bj-raldifsn

Description: All elements in a set satisfy a given property if and only if all but one satisfy that property and that one also does. Typically, this can be used for characterizations that are proved using different methods for a given element and for all others, for instance zero and nonzero numbers, or the empty set and nonempty sets. (Contributed by BJ, 7-Dec-2021)

	Ref	Expression
Hypothesis	bj-raldifsn.is	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
Assertion	bj-raldifsn	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) 𝜑 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-raldifsn.is	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
2		difsnid	⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 )
3	2	eqcomd	⊢ ( 𝐵 ∈ 𝐴 → 𝐴 = ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) )
4	3	raleqdv	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) 𝜑 ) )
5		ralunb	⊢ ( ∀ 𝑥 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) 𝜑 ↔ ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) 𝜑 ∧ ∀ 𝑥 ∈ { 𝐵 } 𝜑 ) )
6	5	a1i	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) 𝜑 ↔ ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) 𝜑 ∧ ∀ 𝑥 ∈ { 𝐵 } 𝜑 ) ) )
7	1	ralsng	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ { 𝐵 } 𝜑 ↔ 𝜓 ) )
8	7	anbi2d	⊢ ( 𝐵 ∈ 𝐴 → ( ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) 𝜑 ∧ ∀ 𝑥 ∈ { 𝐵 } 𝜑 ) ↔ ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) 𝜑 ∧ 𝜓 ) ) )
9	4 6 8	3bitrd	⊢ ( 𝐵 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ( ∀ 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) 𝜑 ∧ 𝜓 ) ) )