Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-raldifsn Structured version   Visualization version   GIF version

Theorem bj-raldifsn 33386
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.es (𝑥 = 𝐵 → (𝜑𝜓))
Assertion
Ref Expression
bj-raldifsn (𝐵𝐴 → (∀𝑥𝐴 𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑𝜓)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem bj-raldifsn
StepHypRef Expression
1 difsnid 4476 . . . 4 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
21eqcomd 2777 . . 3 (𝐵𝐴𝐴 = ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
32raleqdv 3293 . 2 (𝐵𝐴 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑))
4 ralunb 3945 . . 3 (∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
54a1i 11 . 2 (𝐵𝐴 → (∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)))
6 df-ral 3066 . . . 4 (∀𝑥 ∈ {𝐵}𝜑 ↔ ∀𝑥(𝑥 ∈ {𝐵} → 𝜑))
7 velsn 4332 . . . . . . 7 (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
87imbi1i 338 . . . . . 6 ((𝑥 ∈ {𝐵} → 𝜑) ↔ (𝑥 = 𝐵𝜑))
98albii 1895 . . . . 5 (∀𝑥(𝑥 ∈ {𝐵} → 𝜑) ↔ ∀𝑥(𝑥 = 𝐵𝜑))
10 nfv 1995 . . . . . 6 𝑥𝜓
11 bj-raldifsn.es . . . . . 6 (𝑥 = 𝐵 → (𝜑𝜓))
1210, 11bj-ceqsalgv 33209 . . . . 5 (𝐵𝐴 → (∀𝑥(𝑥 = 𝐵𝜑) ↔ 𝜓))
139, 12syl5bb 272 . . . 4 (𝐵𝐴 → (∀𝑥(𝑥 ∈ {𝐵} → 𝜑) ↔ 𝜓))
146, 13syl5bb 272 . . 3 (𝐵𝐴 → (∀𝑥 ∈ {𝐵}𝜑𝜓))
1514anbi2d 614 . 2 (𝐵𝐴 → ((∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑𝜓)))
163, 5, 153bitrd 294 1 (𝐵𝐴 → (∀𝑥𝐴 𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wal 1629   = wceq 1631  wcel 2145  wral 3061  cdif 3720  cun 3721  {csn 4316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-sn 4317
This theorem is referenced by:  bj-0int  33387
  Copyright terms: Public domain W3C validator