Metamath Proof Explorer

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 ⊢ x = B → φ ↔ ψ
Assertion bj-raldifsn ⊢ B ∈ A → ∀ x ∈ A φ ↔ ∀ x ∈ A ∖ B φ ∧ ψ

Proof

Step Hyp Ref Expression
1 bj-raldifsn.is ⊢ x = B → φ ↔ ψ
2 difsnid ⊢ B ∈ A → A ∖ B ∪ B = A
3 2 eqcomd ⊢ B ∈ A → A = A ∖ B ∪ B
4 3 raleqdv ⊢ B ∈ A → ∀ x ∈ A φ ↔ ∀ x ∈ A ∖ B ∪ B φ
5 ralunb ⊢ ∀ x ∈ A ∖ B ∪ B φ ↔ ∀ x ∈ A ∖ B φ ∧ ∀ x ∈ B φ
6 5 a1i ⊢ B ∈ A → ∀ x ∈ A ∖ B ∪ B φ ↔ ∀ x ∈ A ∖ B φ ∧ ∀ x ∈ B φ
7 1 ralsng ⊢ B ∈ A → ∀ x ∈ B φ ↔ ψ
8 7 anbi2d ⊢ B ∈ A → ∀ x ∈ A ∖ B φ ∧ ∀ x ∈ B φ ↔ ∀ x ∈ A ∖ B φ ∧ ψ
9 4 6 8 3bitrd ⊢ B ∈ A → ∀ x ∈ A φ ↔ ∀ x ∈ A ∖ B φ ∧ ψ