Theorem disjxsn

Description: A singleton collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	disjxsn	$$⊢\underset{x\in \left\{A\right\}}{Disj}B$$

Proof

Step	Hyp	Ref	Expression
1		dfdisj2	$$⊢\underset{x\in \left\{A\right\}}{Disj}B\leftrightarrow \forall y{\exists }^{*}x\left(x\in \left\{A\right\}\wedge y\in B\right)$$
2		moeq	$$⊢{\exists }^{*}xx=A$$
3		elsni	$$⊢x\in \left\{A\right\}\to x=A$$
4	3	adantr	$$⊢\left(x\in \left\{A\right\}\wedge y\in B\right)\to x=A$$
5	4	moimi	$$⊢{\exists }^{*}xx=A\to {\exists }^{*}x\left(x\in \left\{A\right\}\wedge y\in B\right)$$
6	2 5	ax-mp	$$⊢{\exists }^{*}x\left(x\in \left\{A\right\}\wedge y\in B\right)$$
7	1 6	mpgbir	$$⊢\underset{x\in \left\{A\right\}}{Disj}B$$