Theorem csbiebt

Description: Conversion of implicit substitution to explicit substitution into a class. (Closed theorem version of csbiegf .) (Contributed by NM, 11-Nov-2005)

	Ref	Expression
Assertion	csbiebt	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}xC\right)\to \left(\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		spsbc	$$⊢A\in \mathrm{V}\to \left(\forall x\left(x=A\to B=C\right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(x=A\to B=C\right)\right)$$
3	2	adantr	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to \left(\forall x\left(x=A\to B=C\right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(x=A\to B=C\right)\right)$$
4		simpl	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to A\in \mathrm{V}$$
5		biimt	$$⊢x=A\to \left(B=C\leftrightarrow \left(x=A\to B=C\right)\right)$$
6		csbeq1a	$$⊢x=A\to B=⦋A/x⦌B$$
7	6	eqeq1d	$$⊢x=A\to \left(B=C\leftrightarrow ⦋A/x⦌B=C\right)$$
8	5 7	bitr3d	$$⊢x=A\to \left(\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$
9	8	adantl	$$⊢\left(\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\wedge x=A\right)\to \left(\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$
10		nfv	$$⊢ℲxA\in \mathrm{V}$$
11		nfnfc1	$$⊢Ⅎx\underset{\_}{Ⅎ}xC$$
12	10 11	nfan	$$⊢Ⅎx\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)$$
13		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋A/x⦌B$$
14	13	a1i	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to \underset{\_}{Ⅎ}x⦋A/x⦌B$$
15		simpr	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to \underset{\_}{Ⅎ}xC$$
16	14 15	nfeqd	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to Ⅎx⦋A/x⦌B=C$$
17	4 9 12 16	sbciedf	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$
18	3 17	sylibd	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to \left(\forall x\left(x=A\to B=C\right)\to ⦋A/x⦌B=C\right)$$
19	13	a1i	$$⊢\underset{\_}{Ⅎ}xC\to \underset{\_}{Ⅎ}x⦋A/x⦌B$$
20		id	$$⊢\underset{\_}{Ⅎ}xC\to \underset{\_}{Ⅎ}xC$$
21	19 20	nfeqd	$$⊢\underset{\_}{Ⅎ}xC\to Ⅎx⦋A/x⦌B=C$$
22	11 21	nfan1	$$⊢Ⅎx\left(\underset{\_}{Ⅎ}xC\wedge ⦋A/x⦌B=C\right)$$
23	7	biimprcd	$$⊢⦋A/x⦌B=C\to \left(x=A\to B=C\right)$$
24	23	adantl	$$⊢\left(\underset{\_}{Ⅎ}xC\wedge ⦋A/x⦌B=C\right)\to \left(x=A\to B=C\right)$$
25	22 24	alrimi	$$⊢\left(\underset{\_}{Ⅎ}xC\wedge ⦋A/x⦌B=C\right)\to \forall x\left(x=A\to B=C\right)$$
26	25	ex	$$⊢\underset{\_}{Ⅎ}xC\to \left(⦋A/x⦌B=C\to \forall x\left(x=A\to B=C\right)\right)$$
27	26	adantl	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to \left(⦋A/x⦌B=C\to \forall x\left(x=A\to B=C\right)\right)$$
28	18 27	impbid	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}xC\right)\to \left(\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$
29	1 28	sylan	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}xC\right)\to \left(\forall x\left(x=A\to B=C\right)\leftrightarrow ⦋A/x⦌B=C\right)$$