Theorem csbima12gALTVD

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

	Ref	Expression
Assertion	csbima12gALTVD	$$⊢A\in C\to ⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\in C\to A\in C\right)$$
2		csbres	$$⊢⦋A/x⦌\left({F\upharpoonright }_B\right)={⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}$$
3	2	a1i	$$⊢A\in C\to ⦋A/x⦌\left({F\upharpoonright }_B\right)={⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}$$
4	1 3	e1a	$$⊢\left(A\in C\to ⦋A/x⦌\left({F\upharpoonright }_B\right)={⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)$$
5		rneq	$$⊢⦋A/x⦌\left({F\upharpoonright }_B\right)={⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\to \mathrm{ran}⦋A/x⦌\left({F\upharpoonright }_B\right)=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)$$
6	4 5	e1a	$$⊢\left(A\in C\to \mathrm{ran}⦋A/x⦌\left({F\upharpoonright }_B\right)=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\right)$$
7		csbrn	$$⊢⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}⦋A/x⦌\left({F\upharpoonright }_B\right)$$
8	7	a1i	$$⊢A\in C\to ⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}⦋A/x⦌\left({F\upharpoonright }_B\right)$$
9	1 8	e1a	$$⊢\left(A\in C\to ⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}⦋A/x⦌\left({F\upharpoonright }_B\right)\right)$$
10		eqeq2	$$⊢\mathrm{ran}⦋A/x⦌\left({F\upharpoonright }_B\right)=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\to \left(⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}⦋A/x⦌\left({F\upharpoonright }_B\right)\leftrightarrow ⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\right)$$
11	10	biimpd	$$⊢\mathrm{ran}⦋A/x⦌\left({F\upharpoonright }_B\right)=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\to \left(⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}⦋A/x⦌\left({F\upharpoonright }_B\right)\to ⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\right)$$
12	6 9 11	e11	$$⊢\left(A\in C\to ⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\right)$$
13		df-ima	$$⊢F\left[B\right]=\mathrm{ran}\left({F\upharpoonright }_B\right)$$
14	13	ax-gen	$$⊢\forall xF\left[B\right]=\mathrm{ran}\left({F\upharpoonright }_B\right)$$
15		csbeq2	$$⊢\forall xF\left[B\right]=\mathrm{ran}\left({F\upharpoonright }_B\right)\to ⦋A/x⦌F\left[B\right]=⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)$$
16	15	a1i	$$⊢A\in C\to \left(\forall xF\left[B\right]=\mathrm{ran}\left({F\upharpoonright }_B\right)\to ⦋A/x⦌F\left[B\right]=⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)\right)$$
17	1 14 16	e10	$$⊢\left(A\in C\to ⦋A/x⦌F\left[B\right]=⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)\right)$$
18		eqeq2	$$⊢⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\to \left(⦋A/x⦌F\left[B\right]=⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)\leftrightarrow ⦋A/x⦌F\left[B\right]=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\right)$$
19	18	biimpd	$$⊢⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\to \left(⦋A/x⦌F\left[B\right]=⦋A/x⦌\mathrm{ran}\left({F\upharpoonright }_B\right)\to ⦋A/x⦌F\left[B\right]=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\right)$$
20	12 17 19	e11	$$⊢\left(A\in C\to ⦋A/x⦌F\left[B\right]=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\right)$$
21		df-ima	$$⊢⦋A/x⦌F\left[⦋A/x⦌B\right]=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)$$
22		eqeq2	$$⊢⦋A/x⦌F\left[⦋A/x⦌B\right]=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\to \left(⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]\leftrightarrow ⦋A/x⦌F\left[B\right]=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\right)$$
23	22	biimprcd	$$⊢⦋A/x⦌F\left[B\right]=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\to \left(⦋A/x⦌F\left[⦋A/x⦌B\right]=\mathrm{ran}\left({⦋A/x⦌F\upharpoonright }_{⦋A/x⦌B}\right)\to ⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]\right)$$
24	20 21 23	e10	$$⊢\left(A\in C\to ⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]\right)$$
25	24	in1	$$⊢A\in C\to ⦋A/x⦌F\left[B\right]=⦋A/x⦌F\left[⦋A/x⦌B\right]$$