Theorem csbrngVD

Description: Virtual deduction proof of csbrn . 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. csbrn is csbrngVD without virtual deductions and was automatically derived from csbrngVD .

	Ref	Expression
Assertion	csbrngVD	$$⊢A\in V\to ⦋A/x⦌\mathrm{ran}B=\mathrm{ran}⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\in V\to A\in V\right)$$
2		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⦋A/x⦌⟨w,y⟩\in ⦋A/x⦌B$$
3	2	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⦋A/x⦌⟨w,y⟩\in ⦋A/x⦌B\right)$$
4	1 3	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⦋A/x⦌⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
5		csbconstg	$$⊢A\in V\to ⦋A/x⦌⟨w,y⟩=⟨w,y⟩$$
6	1 5	e1a	$$⊢\left(A\in V\to ⦋A/x⦌⟨w,y⟩=⟨w,y⟩\right)$$
7		eleq1	$$⊢⦋A/x⦌⟨w,y⟩=⟨w,y⟩\to \left(⦋A/x⦌⟨w,y⟩\in ⦋A/x⦌B\leftrightarrow ⟨w,y⟩\in ⦋A/x⦌B\right)$$
8	6 7	e1a	$$⊢\left(A\in V\to \left(⦋A/x⦌⟨w,y⟩\in ⦋A/x⦌B\leftrightarrow ⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
9		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⦋A/x⦌⟨w,y⟩\in ⦋A/x⦌B\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⟨w,y⟩\in ⦋A/x⦌B\right)\leftrightarrow \left(⦋A/x⦌⟨w,y⟩\in ⦋A/x⦌B\leftrightarrow ⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
10	9	biimprd	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⦋A/x⦌⟨w,y⟩\in ⦋A/x⦌B\right)\to \left(\left(⦋A/x⦌⟨w,y⟩\in ⦋A/x⦌B\leftrightarrow ⟨w,y⟩\in ⦋A/x⦌B\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
11	4 8 10	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
12	11	gen11	$$⊢\left(A\in V\to \forall w\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
13		exbi	$$⊢\forall w\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow ⟨w,y⟩\in ⦋A/x⦌B\right)\to \left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)$$
14	12 13	e1a	$$⊢\left(A\in V\to \left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
15		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\leftrightarrow \exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B$$
16	15	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\leftrightarrow \exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\right)$$
17	16	bicomd	$$⊢A\in V\to \left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right)$$
18	1 17	e1a	$$⊢\left(A\in V\to \left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right)\right)$$
19		bitr3	$$⊢\left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right)\to \left(\left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
20	19	com12	$$⊢\left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)\to \left(\left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}⟨w,y⟩\in B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
21	14 18 20	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
22	21	gen11	$$⊢\left(A\in V\to \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)\right)$$
23		abbib	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\leftrightarrow \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)$$
24	23	biimpri	$$⊢\forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\leftrightarrow \exists w⟨w,y⟩\in ⦋A/x⦌B\right)\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}$$
25	22 24	e1a	$$⊢\left(A\in V\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\right)$$
26		csbab	$$⊢⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}$$
27	26	a1i	$$⊢A\in V\to ⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}$$
28	1 27	e1a	$$⊢\left(A\in V\to ⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}\right)$$
29		eqeq2	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\to \left(⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}\leftrightarrow ⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\right)$$
30	29	biimpd	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\to \left(⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w⟨w,y⟩\in B\right\}\to ⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\right)$$
31	25 28 30	e11	$$⊢\left(A\in V\to ⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\right)$$
32		dfrn3	$$⊢\mathrm{ran}B=\left\{y|\exists w⟨w,y⟩\in B\right\}$$
33	32	ax-gen	$$⊢\forall x\mathrm{ran}B=\left\{y|\exists w⟨w,y⟩\in B\right\}$$
34		csbeq2	$$⊢\forall x\mathrm{ran}B=\left\{y|\exists w⟨w,y⟩\in B\right\}\to ⦋A/x⦌\mathrm{ran}B=⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}$$
35	34	a1i	$$⊢A\in V\to \left(\forall x\mathrm{ran}B=\left\{y|\exists w⟨w,y⟩\in B\right\}\to ⦋A/x⦌\mathrm{ran}B=⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}\right)$$
36	1 33 35	e10	$$⊢\left(A\in V\to ⦋A/x⦌\mathrm{ran}B=⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}\right)$$
37		eqeq2	$$⊢⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\to \left(⦋A/x⦌\mathrm{ran}B=⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}\leftrightarrow ⦋A/x⦌\mathrm{ran}B=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\right)$$
38	37	biimpd	$$⊢⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\to \left(⦋A/x⦌\mathrm{ran}B=⦋A/x⦌\left\{y|\exists w⟨w,y⟩\in B\right\}\to ⦋A/x⦌\mathrm{ran}B=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\right)$$
39	31 36 38	e11	$$⊢\left(A\in V\to ⦋A/x⦌\mathrm{ran}B=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\right)$$
40		dfrn3	$$⊢\mathrm{ran}⦋A/x⦌B=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}$$
41		eqeq2	$$⊢\mathrm{ran}⦋A/x⦌B=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\to \left(⦋A/x⦌\mathrm{ran}B=\mathrm{ran}⦋A/x⦌B\leftrightarrow ⦋A/x⦌\mathrm{ran}B=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\right)$$
42	41	biimprcd	$$⊢⦋A/x⦌\mathrm{ran}B=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\to \left(\mathrm{ran}⦋A/x⦌B=\left\{y|\exists w⟨w,y⟩\in ⦋A/x⦌B\right\}\to ⦋A/x⦌\mathrm{ran}B=\mathrm{ran}⦋A/x⦌B\right)$$
43	39 40 42	e10	$$⊢\left(A\in V\to ⦋A/x⦌\mathrm{ran}B=\mathrm{ran}⦋A/x⦌B\right)$$
44	43	in1	$$⊢A\in V\to ⦋A/x⦌\mathrm{ran}B=\mathrm{ran}⦋A/x⦌B$$