Theorem bj-raldifsn 36710

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.)

Hypothesis

Ref	Expression
bj-raldifsn.is	⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem bj-raldifsn

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3050   ∖ cdif 3941   ∪ cun 3942  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-sn 4631

This theorem is referenced by:  bj-0int  36711