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 35041
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
StepHypRef Expression
1 difsnid 4739 . . . 4 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
21eqcomd 2745 . . 3 (𝐵𝐴𝐴 = ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
32raleqdv 3340 . 2 (𝐵𝐴 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑))
4 ralunb 4121 . . 3 (∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
54a1i 11 . 2 (𝐵𝐴 → (∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)))
6 bj-raldifsn.is . . . 4 (𝑥 = 𝐵 → (𝜑𝜓))
76ralsng 4605 . . 3 (𝐵𝐴 → (∀𝑥 ∈ {𝐵}𝜑𝜓))
87anbi2d 632 . 2 (𝐵𝐴 → ((∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑𝜓)))
93, 5, 83bitrd 308 1 (𝐵𝐴 → (∀𝑥𝐴 𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2112  wral 3064  cdif 3880  cun 3881  {csn 4557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4558
This theorem is referenced by:  bj-0int  35042
  Copyright terms: Public domain W3C validator