Theorem elpreqprlem

Description: Lemma for elpreqpr . (Contributed by Scott Fenton, 7-Dec-2020) (Revised by AV, 9-Dec-2020)

	Ref	Expression
Assertion	elpreqprlem	$$⊢B\in V\to \exists x\left\{B,C\right\}=\left\{B,x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{B,C\right\}=\left\{B,C\right\}$$
2		preq2	$$⊢x=C\to \left\{B,x\right\}=\left\{B,C\right\}$$
3	2	eqeq2d	$$⊢x=C\to \left(\left\{B,C\right\}=\left\{B,x\right\}\leftrightarrow \left\{B,C\right\}=\left\{B,C\right\}\right)$$
4	3	spcegv	$$⊢C\in \mathrm{V}\to \left(\left\{B,C\right\}=\left\{B,C\right\}\to \exists x\left\{B,C\right\}=\left\{B,x\right\}\right)$$
5	1 4	mpi	$$⊢C\in \mathrm{V}\to \exists x\left\{B,C\right\}=\left\{B,x\right\}$$
6	5	a1d	$$⊢C\in \mathrm{V}\to \left(B\in V\to \exists x\left\{B,C\right\}=\left\{B,x\right\}\right)$$
7		dfsn2	$$⊢\left\{B\right\}=\left\{B,B\right\}$$
8		preq2	$$⊢x=B\to \left\{B,x\right\}=\left\{B,B\right\}$$
9	8	eqeq2d	$$⊢x=B\to \left(\left\{B\right\}=\left\{B,x\right\}\leftrightarrow \left\{B\right\}=\left\{B,B\right\}\right)$$
10	9	spcegv	$$⊢B\in V\to \left(\left\{B\right\}=\left\{B,B\right\}\to \exists x\left\{B\right\}=\left\{B,x\right\}\right)$$
11	7 10	mpi	$$⊢B\in V\to \exists x\left\{B\right\}=\left\{B,x\right\}$$
12		prprc2	$$⊢\neg C\in \mathrm{V}\to \left\{B,C\right\}=\left\{B\right\}$$
13	12	eqeq1d	$$⊢\neg C\in \mathrm{V}\to \left(\left\{B,C\right\}=\left\{B,x\right\}\leftrightarrow \left\{B\right\}=\left\{B,x\right\}\right)$$
14	13	exbidv	$$⊢\neg C\in \mathrm{V}\to \left(\exists x\left\{B,C\right\}=\left\{B,x\right\}\leftrightarrow \exists x\left\{B\right\}=\left\{B,x\right\}\right)$$
15	11 14	imbitrrid	$$⊢\neg C\in \mathrm{V}\to \left(B\in V\to \exists x\left\{B,C\right\}=\left\{B,x\right\}\right)$$
16	6 15	pm2.61i	$$⊢B\in V\to \exists x\left\{B,C\right\}=\left\{B,x\right\}$$