This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 , 𝐴 , ∅ )