Theorem oppcmndclem

Description: Lemma for oppcmndc . Everything is true for two distinct elements in a singleton or an empty set (since it is impossible). Note that if this theorem and oppcendc are in -. x = y form, then both proofs should be one step shorter. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypothesis	oppcmndclem.1	$$⊢\phi \to B=\left\{A\right\}$$
Assertion	oppcmndclem	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(X\ne Y\to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		oppcmndclem.1	$$⊢\phi \to B=\left\{A\right\}$$
2		df-ne	$$⊢X\ne Y\leftrightarrow \neg X=Y$$
3		eqeq1	$$⊢x=X\to \left(x=y\leftrightarrow X=y\right)$$
4		eqeq2	$$⊢y=Y\to \left(X=y\leftrightarrow X=Y\right)$$
5		mosn	$$⊢B=\left\{A\right\}\to {\exists }^{*}xx\in B$$
6	1 5	syl	$$⊢\phi \to {\exists }^{*}xx\in B$$
7		moel	$$⊢{\exists }^{*}xx\in B\leftrightarrow \forall x\in B\forall y\in Bx=y$$
8	6 7	sylib	$$⊢\phi \to \forall x\in B\forall y\in Bx=y$$
9	8	adantr	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \forall x\in B\forall y\in Bx=y$$
10		simprl	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X\in B$$
11		simprr	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to Y\in B$$
12	3 4 9 10 11	rspc2dv	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X=Y$$
13	12	pm2.24d	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(\neg X=Y\to \psi \right)$$
14	2 13	biimtrid	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(X\ne Y\to \psi \right)$$