Theorem bj-raldifsn 37301

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 4766	. . . 4 ⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
2	1	eqcomd 2742	. . 3 ⊢ (𝐵 ∈ 𝐴 → 𝐴 = ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
3	2	raleqdv 3296	. 2 ⊢ (𝐵 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑))
4		ralunb 4149	. . 3 ⊢ (∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
5	4	a1i 11	. 2 ⊢ (𝐵 ∈ 𝐴 → (∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)))
6		bj-raldifsn.is	. . . 4 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
7	6	ralsng 4632	. . 3 ⊢ (𝐵 ∈ 𝐴 → (∀𝑥 ∈ {𝐵}𝜑 ↔ 𝜓))
8	7	anbi2d 630	. 2 ⊢ (𝐵 ∈ 𝐴 → ((∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ 𝜓)))
9	3, 5, 8	3bitrd 305	1 ⊢ (𝐵 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051   ∖ cdif 3898   ∪ cun 3899  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-sn 4581

This theorem is referenced by:  bj-0int  37302