Theorem csbfv12gALTVD

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

	Ref	Expression
Assertion	csbfv12gALTVD	$$⊢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		sbceqg	$$⊢A\in C\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌\left\{y\right\}\right)$$
3	1 2	e1a	$$⊢\left(A\in C\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌\left\{y\right\}\right)\right)$$
4		csbima12	$$⊢⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[⦋A/x⦌\left\{B\right\}\right]$$
5	4	a1i	$$⊢A\in C\to ⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[⦋A/x⦌\left\{B\right\}\right]$$
6	1 5	e1a	$$⊢\left(A\in C\to ⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[⦋A/x⦌\left\{B\right\}\right]\right)$$
7		csbsng	$$⊢A\in C\to ⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}$$
8	1 7	e1a	$$⊢\left(A\in C\to ⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}\right)$$
9		imaeq2	$$⊢⦋A/x⦌\left\{B\right\}=\left\{⦋A/x⦌B\right\}\to ⦋A/x⦌F\left[⦋A/x⦌\left\{B\right\}\right]=⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]$$
10	8 9	e1a	$$⊢\left(A\in C\to ⦋A/x⦌F\left[⦋A/x⦌\left\{B\right\}\right]=⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]\right)$$
11		eqeq1	$$⊢⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[⦋A/x⦌\left\{B\right\}\right]\to \left(⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]\leftrightarrow ⦋A/x⦌F\left[⦋A/x⦌\left\{B\right\}\right]=⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]\right)$$
12	11	biimprd	$$⊢⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[⦋A/x⦌\left\{B\right\}\right]\to \left(⦋A/x⦌F\left[⦋A/x⦌\left\{B\right\}\right]=⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]\to ⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]\right)$$
13	6 10 12	e11	$$⊢\left(A\in C\to ⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]\right)$$
14		csbconstg	$$⊢A\in C\to ⦋A/x⦌\left\{y\right\}=\left\{y\right\}$$
15	1 14	e1a	$$⊢\left(A\in C\to ⦋A/x⦌\left\{y\right\}=\left\{y\right\}\right)$$
16		eqeq12	$$⊢\left(⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]\wedge ⦋A/x⦌\left\{y\right\}=\left\{y\right\}\right)\to \left(⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)$$
17	16	ex	$$⊢⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]\to \left(⦋A/x⦌\left\{y\right\}=\left\{y\right\}\to \left(⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)\right)$$
18	13 15 17	e11	$$⊢\left(A\in C\to \left(⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)\right)$$
19		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌\left\{y\right\}\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)\leftrightarrow \left(⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)\right)$$
20	19	biimprd	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌\left\{y\right\}\right)\to \left(\left(⦋A/x⦌F\left[\left\{B\right\}\right]=⦋A/x⦌\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)\right)$$
21	3 18 20	e11	$$⊢\left(A\in C\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)\right)$$
22	21	gen11	$$⊢\left(A\in C\to \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)\right)$$
23		abbib	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\leftrightarrow \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)$$
24	23	biimpri	$$⊢\forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\leftrightarrow ⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right)\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}$$
25	22 24	e1a	$$⊢\left(A\in C\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
26		csbab	$$⊢⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}$$
27	26	a1i	$$⊢A\in C\to ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}$$
28	1 27	e1a	$$⊢\left(A\in C\to ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\right)$$
29		eqeq2	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to \left(⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\leftrightarrow ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
30	29	biimpd	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to \left(⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\to ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
31	25 28 30	e11	$$⊢\left(A\in C\to ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
32		unieq	$$⊢⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to \bigcup ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}$$
33	31 32	e1a	$$⊢\left(A\in C\to \bigcup ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
34		csbuni	$$⊢⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}$$
35	34	a1i	$$⊢A\in C\to ⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}$$
36	1 35	e1a	$$⊢\left(A\in C\to ⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\right)$$
37		eqeq2	$$⊢\bigcup ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to \left(⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\leftrightarrow ⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
38	37	biimpd	$$⊢\bigcup ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to \left(⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup ⦋A/x⦌\left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\to ⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
39	33 36 38	e11	$$⊢\left(A\in C\to ⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
40		dffv4	$$⊢F\left(B\right)=\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}$$
41	40	ax-gen	$$⊢\forall xF\left(B\right)=\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}$$
42		csbeq2	$$⊢\forall xF\left(B\right)=\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\to ⦋A/x⦌F\left(B\right)=⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}$$
43	42	a1i	$$⊢A\in C\to \left(\forall xF\left(B\right)=\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\to ⦋A/x⦌F\left(B\right)=⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\right)$$
44	1 41 43	e10	$$⊢\left(A\in C\to ⦋A/x⦌F\left(B\right)=⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\right)$$
45		eqeq2	$$⊢⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to \left(⦋A/x⦌F\left(B\right)=⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\leftrightarrow ⦋A/x⦌F\left(B\right)=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
46	45	biimpd	$$⊢⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to \left(⦋A/x⦌F\left(B\right)=⦋A/x⦌\bigcup \left\{y|F\left[\left\{B\right\}\right]=\left\{y\right\}\right\}\to ⦋A/x⦌F\left(B\right)=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
47	39 44 46	e11	$$⊢\left(A\in C\to ⦋A/x⦌F\left(B\right)=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
48		dffv4	$$⊢⦋A/x⦌F\left(⦋A/x⦌B\right)=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}$$
49		eqeq2	$$⊢⦋A/x⦌F\left(⦋A/x⦌B\right)=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to \left(⦋A/x⦌F\left(B\right)=⦋A/x⦌F\left(⦋A/x⦌B\right)\leftrightarrow ⦋A/x⦌F\left(B\right)=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\right)$$
50	49	biimprcd	$$⊢⦋A/x⦌F\left(B\right)=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to \left(⦋A/x⦌F\left(⦋A/x⦌B\right)=\bigcup \left\{y|⦋A/x⦌F\left[\left\{⦋A/x⦌B\right\}\right]=\left\{y\right\}\right\}\to ⦋A/x⦌F\left(B\right)=⦋A/x⦌F\left(⦋A/x⦌B\right)\right)$$
51	47 48 50	e10	$$⊢\left(A\in C\to ⦋A/x⦌F\left(B\right)=⦋A/x⦌F\left(⦋A/x⦌B\right)\right)$$
52	51	in1	$$⊢A\in C\to ⦋A/x⦌F\left(B\right)=⦋A/x⦌F\left(⦋A/x⦌B\right)$$