Theorem csbsngVD

Description: Virtual deduction proof of csbsng . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbsng is csbsngVD without virtual deductions and was automatically derived from csbsngVD .

	Ref	Expression
Assertion	csbsngVD	$$⊢A\in V\to ⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\in V\to A\in V\right)$$
2		sbceqg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow ⦋A/x⦌y=⦋A/x⦌B\right)$$
3	1 2	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow ⦋A/x⦌y=⦋A/x⦌B\right)\right)$$
4		csbconstg	$$⊢A\in V\to ⦋A/x⦌y=y$$
5	1 4	e1a	$$⊢\left(A\in V\to ⦋A/x⦌y=y\right)$$
6		eqeq1	$$⊢⦋A/x⦌y=y\to \left(⦋A/x⦌y=⦋A/x⦌B\leftrightarrow y=⦋A/x⦌B\right)$$
7	5 6	e1a	$$⊢\left(A\in V\to \left(⦋A/x⦌y=⦋A/x⦌B\leftrightarrow y=⦋A/x⦌B\right)\right)$$
8		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow ⦋A/x⦌y=⦋A/x⦌B\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow y=⦋A/x⦌B\right)\leftrightarrow \left(⦋A/x⦌y=⦋A/x⦌B\leftrightarrow y=⦋A/x⦌B\right)\right)$$
9	8	biimprd	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow ⦋A/x⦌y=⦋A/x⦌B\right)\to \left(\left(⦋A/x⦌y=⦋A/x⦌B\leftrightarrow y=⦋A/x⦌B\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow y=⦋A/x⦌B\right)\right)$$
10	3 7 9	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow y=⦋A/x⦌B\right)\right)$$
11	10	gen11	$$⊢\left(A\in V\to \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow y=⦋A/x⦌B\right)\right)$$
12		abbib	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}\leftrightarrow \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow y=⦋A/x⦌B\right)$$
13	12	biimpri	$$⊢\forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow y=⦋A/x⦌B\right)\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}$$
14	11 13	e1a	$$⊢\left(A\in V\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}\right)$$
15		csbab	$$⊢⦋A/x⦌\left\{y|y=B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}$$
16	15	a1i	$$⊢A\in V\to ⦋A/x⦌\left\{y|y=B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}$$
17	16	eqcomd	$$⊢A\in V\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=⦋A/x⦌\left\{y|y=B\right\}$$
18	1 17	e1a	$$⊢\left(A\in V\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=⦋A/x⦌\left\{y|y=B\right\}\right)$$
19		eqeq1	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=⦋A/x⦌\left\{y|y=B\right\}\to \left(\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}\leftrightarrow ⦋A/x⦌\left\{y|y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}\right)$$
20	19	biimpcd	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}\to \left(\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\right\}=⦋A/x⦌\left\{y|y=B\right\}\to ⦋A/x⦌\left\{y|y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}\right)$$
21	14 18 20	e11	$$⊢\left(A\in V\to ⦋A/x⦌\left\{y|y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}\right)$$
22		df-sn	$$⊢\left\{B\right\}=\left\{y|y=B\right\}$$
23	22	ax-gen	$$⊢\forall x\left\{B\right\}=\left\{y|y=B\right\}$$
24		csbeq2	$$⊢\forall x\left\{B\right\}=\left\{y|y=B\right\}\to ⦋A/x⦌\left\{B\right\}=⦋A/x⦌\left\{y|y=B\right\}$$
25	24	a1i	$$⊢A\in V\to \left(\forall x\left\{B\right\}=\left\{y|y=B\right\}\to ⦋A/x⦌\left\{B\right\}=⦋A/x⦌\left\{y|y=B\right\}\right)$$
26	1 23 25	e10	$$⊢\left(A\in V\to ⦋A/x⦌\left\{B\right\}=⦋A/x⦌\left\{y|y=B\right\}\right)$$
27		eqeq2	$$⊢⦋A/x⦌\left\{y|y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}\to \left(⦋A/x⦌\left\{B\right\}=⦋A/x⦌\left\{y|y=B\right\}\leftrightarrow ⦋A/x⦌\left\{B\right\}=\left\{y|y=⦋A/x⦌B\right\}\right)$$
28	27	biimpd	$$⊢⦋A/x⦌\left\{y|y=B\right\}=\left\{y|y=⦋A/x⦌B\right\}\to \left(⦋A/x⦌\left\{B\right\}=⦋A/x⦌\left\{y|y=B\right\}\to ⦋A/x⦌\left\{B\right\}=\left\{y|y=⦋A/x⦌B\right\}\right)$$
29	21 26 28	e11	$$⊢\left(A\in V\to ⦋A/x⦌\left\{B\right\}=\left\{y|y=⦋A/x⦌B\right\}\right)$$
30		df-sn	$$⊢\left\{⦋A/x⦌B\right\}=\left\{y|y=⦋A/x⦌B\right\}$$
31		eqeq2	$$⊢\left\{⦋A/x⦌B\right\}=\left\{y|y=⦋A/x⦌B\right\}\to \left(⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}\leftrightarrow ⦋A/x⦌\left\{B\right\}=\left\{y|y=⦋A/x⦌B\right\}\right)$$
32	31	biimprcd	$$⊢⦋A/x⦌\left\{B\right\}=\left\{y|y=⦋A/x⦌B\right\}\to \left(\left\{⦋A/x⦌B\right\}=\left\{y|y=⦋A/x⦌B\right\}\to ⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}\right)$$
33	29 30 32	e10	$$⊢\left(A\in V\to ⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}\right)$$
34	33	in1	$$⊢A\in V\to ⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}$$