Theorem bj-raldifsn 33054

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	|- ( x = B -> ( ph <-> ps ) )

Assertion

Ref	Expression
bj-raldifsn	|- ( B e. A -> ( A. x e. A ph <-> ( A. x e. ( A \ { B } ) ph /\ ps ) ) )

Distinct variable groups:   x, A   x, B   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem bj-raldifsn

Step	Hyp	Ref	Expression
1		difsnid 4341	. . . 4 |- ( B e. A -> ( ( A \ { B } ) u. { B } ) = A )
2	1	eqcomd 2628	. . 3 |- ( B e. A -> A = ( ( A \ { B } ) u. { B } ) )
3	2	raleqdv 3144	. 2 |- ( B e. A -> ( A. x e. A ph <-> A. x e. ( ( A \ { B } ) u. { B } ) ph ) )
4		ralunb 3794	. . 3 |- ( A. x e. ( ( A \ { B } ) u. { B } ) ph <-> ( A. x e. ( A \ { B } ) ph /\ A. x e. { B } ph ) )
5	4	a1i 11	. 2 |- ( B e. A -> ( A. x e. ( ( A \ { B } ) u. { B } ) ph <-> ( A. x e. ( A \ { B } ) ph /\ A. x e. { B } ph ) ) )
6		df-ral 2917	. . . 4 |- ( A. x e. { B } ph <-> A. x ( x e. { B } -> ph ) )
7		velsn 4193	. . . . . . 7 |- ( x e. { B } <-> x = B )
8	7	imbi1i 339	. . . . . 6 |- ( ( x e. { B } -> ph ) <-> ( x = B -> ph ) )
9	8	albii 1747	. . . . 5 |- ( A. x ( x e. { B } -> ph ) <-> A. x ( x = B -> ph ) )
10		nfv 1843	. . . . . 6 |- F/ x ps
11		bj-raldifsn.es	. . . . . 6 |- ( x = B -> ( ph <-> ps ) )
12	10, 11	bj-ceqsalgv 32880	. . . . 5 |- ( B e. A -> ( A. x ( x = B -> ph ) <-> ps ) )
13	9, 12	syl5bb 272	. . . 4 |- ( B e. A -> ( A. x ( x e. { B } -> ph ) <-> ps ) )
14	6, 13	syl5bb 272	. . 3 |- ( B e. A -> ( A. x e. { B } ph <-> ps ) )
15	14	anbi2d 740	. 2 |- ( B e. A -> ( ( A. x e. ( A \ { B } ) ph /\ A. x e. { B } ph ) <-> ( A. x e. ( A \ { B } ) ph /\ ps ) ) )
16	3, 5, 15	3bitrd 294	1 |- ( B e. A -> ( A. x e. A ph <-> ( A. x e. ( A \ { B } ) ph /\ ps ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   e. wcel 1990   A.wral 2912   \ cdif 3571   u. cun 3572   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178

This theorem is referenced by:  bj-0int  33055