Theorem disjxsn

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

	Ref	Expression
Assertion	disjxsn	⊢ Disj 𝑥 ∈ { 𝐴 } 𝐵

Proof

Step	Hyp	Ref	Expression
1		dfdisj2	⊢ ( Disj 𝑥 ∈ { 𝐴 } 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ 𝐵 ) )
2		moeq	⊢ ∃* 𝑥 𝑥 = 𝐴
3		elsni	⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
4	3	adantr	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ 𝐵 ) → 𝑥 = 𝐴 )
5	4	moimi	⊢ ( ∃* 𝑥 𝑥 = 𝐴 → ∃* 𝑥 ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ 𝐵 ) )
6	2 5	ax-mp	⊢ ∃* 𝑥 ( 𝑥 ∈ { 𝐴 } ∧ 𝑦 ∈ 𝐵 )
7	1 6	mpgbir	⊢ Disj 𝑥 ∈ { 𝐴 } 𝐵