Theorem unisnif

Description: Express union of singleton in terms of if . (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	unisnif	⊢ ∪ { 𝐴 } = if ( 𝐴 ∈ V , 𝐴 , ∅ )

Proof

Step	Hyp	Ref	Expression
1		iftrue	⊢ ( 𝐴 ∈ V → if ( 𝐴 ∈ V , 𝐴 , ∅ ) = 𝐴 )
2		unisng	⊢ ( 𝐴 ∈ V → ∪ { 𝐴 } = 𝐴 )
3	1 2	eqtr4d	⊢ ( 𝐴 ∈ V → if ( 𝐴 ∈ V , 𝐴 , ∅ ) = ∪ { 𝐴 } )
4		iffalse	⊢ ( ¬ 𝐴 ∈ V → if ( 𝐴 ∈ V , 𝐴 , ∅ ) = ∅ )
5		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
6	5	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
7	6	unieqd	⊢ ( ¬ 𝐴 ∈ V → ∪ { 𝐴 } = ∪ ∅ )
8		uni0	⊢ ∪ ∅ = ∅
9	7 8	eqtrdi	⊢ ( ¬ 𝐴 ∈ V → ∪ { 𝐴 } = ∅ )
10	4 9	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → if ( 𝐴 ∈ V , 𝐴 , ∅ ) = ∪ { 𝐴 } )
11	3 10	pm2.61i	⊢ if ( 𝐴 ∈ V , 𝐴 , ∅ ) = ∪ { 𝐴 }
12	11	eqcomi	⊢ ∪ { 𝐴 } = if ( 𝐴 ∈ V , 𝐴 , ∅ )