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 37425
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 4754 . . . 4 (𝐵𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴)
21eqcomd 2743 . . 3 (𝐵𝐴𝐴 = ((𝐴 ∖ {𝐵}) ∪ {𝐵}))
32raleqdv 3296 . 2 (𝐵𝐴 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑))
4 ralunb 4138 . . 3 (∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑))
54a1i 11 . 2 (𝐵𝐴 → (∀𝑥 ∈ ((𝐴 ∖ {𝐵}) ∪ {𝐵})𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑)))
6 bj-raldifsn.is . . . 4 (𝑥 = 𝐵 → (𝜑𝜓))
76ralsng 4620 . . 3 (𝐵𝐴 → (∀𝑥 ∈ {𝐵}𝜑𝜓))
87anbi2d 631 . 2 (𝐵𝐴 → ((∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑 ∧ ∀𝑥 ∈ {𝐵}𝜑) ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑𝜓)))
93, 5, 83bitrd 305 1 (𝐵𝐴 → (∀𝑥𝐴 𝜑 ↔ (∀𝑥 ∈ (𝐴 ∖ {𝐵})𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1542  wcel 2114  wral 3052  cdif 3887  cun 3888  {csn 4568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-sn 4569
This theorem is referenced by:  bj-0int  37426
  Copyright terms: Public domain W3C validator