rabsnifsb

Description: A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 21-Jul-2019)

		Ref	Expression
	Assertion	rabsnifsb	⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ )

Proof

Step	Hyp	Ref	Expression
1		elsni	⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
2		sbceq1a	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
3	2	biimpd	⊢ ( 𝑥 = 𝐴 → ( 𝜑 → [ 𝐴 / 𝑥 ] 𝜑 ) )
4	1 3	syl	⊢ ( 𝑥 ∈ { 𝐴 } → ( 𝜑 → [ 𝐴 / 𝑥 ] 𝜑 ) )
5	4	imdistani	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) → ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )
6	5	orcd	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) → ( ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑥 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
7	2	biimprd	⊢ ( 𝑥 = 𝐴 → ( [ 𝐴 / 𝑥 ] 𝜑 → 𝜑 ) )
8	1 7	syl	⊢ ( 𝑥 ∈ { 𝐴 } → ( [ 𝐴 / 𝑥 ] 𝜑 → 𝜑 ) )
9	8	imdistani	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) → ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) )
10		noel	⊢ ¬ 𝑥 ∈ ∅
11	10	pm2.21i	⊢ ( 𝑥 ∈ ∅ → ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) )
12	11	adantr	⊢ ( ( 𝑥 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) → ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) )
13	9 12	jaoi	⊢ ( ( ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑥 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) → ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) )
14	6 13	impbii	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑥 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
15	14	abbii	⊢ { 𝑥 ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) } = { 𝑥 ∣ ( ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑥 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) }
16		nfv	⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑥 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) )
17		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝐴 }
18		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝐴 / 𝑥 ] 𝜑
19	17 18	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 )
20		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ ∅
21	18	nfn	⊢ Ⅎ 𝑥 ¬ [ 𝐴 / 𝑥 ] 𝜑
22	20 21	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 )
23	19 22	nfor	⊢ Ⅎ 𝑥 ( ( 𝑦 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑦 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) )
24		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝐴 } ↔ 𝑦 ∈ { 𝐴 } ) )
25	24	anbi1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
26		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ∅ ↔ 𝑦 ∈ ∅ ) )
27	26	anbi1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
28	25 27	orbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑥 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) ↔ ( ( 𝑦 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑦 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) ) )
29	16 23 28	cbvabw	⊢ { 𝑥 ∣ ( ( 𝑥 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑥 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) } = { 𝑦 ∣ ( ( 𝑦 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑦 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) }
30	15 29	eqtri	⊢ { 𝑥 ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) } = { 𝑦 ∣ ( ( 𝑦 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑦 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) }
31		df-rab	⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ { 𝐴 } ∧ 𝜑 ) }
32		df-if	⊢ if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = { 𝑦 ∣ ( ( 𝑦 ∈ { 𝐴 } ∧ [ 𝐴 / 𝑥 ] 𝜑 ) ∨ ( 𝑦 ∈ ∅ ∧ ¬ [ 𝐴 / 𝑥 ] 𝜑 ) ) }
33	30 31 32	3eqtr4i	⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ )

Metamath Proof Explorer

Theorem rabsnifsb

Proof