Theorem en2snOLD

Description: Obsolete version of en2sn as of 31-Jul-2024. (Contributed by NM, 9-Nov-2003) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	en2snOLD	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{A\right\}\approx \left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ensn1g	$$⊢A\in C\to \left\{A\right\}\approx 1_{𝑜}$$
2		ensn1g	$$⊢B\in D\to \left\{B\right\}\approx 1_{𝑜}$$
3	2	ensymd	$$⊢B\in D\to 1_{𝑜}\approx \left\{B\right\}$$
4		entr	$$⊢\left(\left\{A\right\}\approx 1_{𝑜}\wedge 1_{𝑜}\approx \left\{B\right\}\right)\to \left\{A\right\}\approx \left\{B\right\}$$
5	1 3 4	syl2an	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{A\right\}\approx \left\{B\right\}$$