Theorem unisn2

Description: A version of unisn without the A e. _V hypothesis. (Contributed by Stefan Allan, 14-Mar-2006)

	Ref	Expression
Assertion	unisn2	⊢ ∪ { 𝐴 } ∈ { ∅ , 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		unisng	⊢ ( 𝐴 ∈ V → ∪ { 𝐴 } = 𝐴 )
2		prid2g	⊢ ( 𝐴 ∈ V → 𝐴 ∈ { ∅ , 𝐴 } )
3	1 2	eqeltrd	⊢ ( 𝐴 ∈ V → ∪ { 𝐴 } ∈ { ∅ , 𝐴 } )
4		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
5	4	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
6	5	unieqd	⊢ ( ¬ 𝐴 ∈ V → ∪ { 𝐴 } = ∪ ∅ )
7		uni0	⊢ ∪ ∅ = ∅
8		0ex	⊢ ∅ ∈ V
9	8	prid1	⊢ ∅ ∈ { ∅ , 𝐴 }
10	7 9	eqeltri	⊢ ∪ ∅ ∈ { ∅ , 𝐴 }
11	6 10	eqeltrdi	⊢ ( ¬ 𝐴 ∈ V → ∪ { 𝐴 } ∈ { ∅ , 𝐴 } )
12	3 11	pm2.61i	⊢ ∪ { 𝐴 } ∈ { ∅ , 𝐴 }