Theorem csbie2df

Description: Conversion of implicit substitution to explicit class substitution. This version of csbiedf avoids a disjointness condition on x , A and x , D by substituting twice. Deduction form of csbie2 . (Contributed by AV, 29-Mar-2024)

	Ref	Expression
Hypotheses	csbie2df.p	$$⊢Ⅎx\phi$$
	csbie2df.c	$$⊢\phi \to \underset{\_}{Ⅎ}xC$$
	csbie2df.d	$$⊢\phi \to \underset{\_}{Ⅎ}xD$$
	csbie2df.a	$$⊢\phi \to A\in V$$
	csbie2df.1	$$⊢\left(\phi \wedge x=y\right)\to B=C$$
	csbie2df.2	$$⊢\left(\phi \wedge y=A\right)\to C=D$$
Assertion	csbie2df	$$⊢\phi \to ⦋A/x⦌B=D$$

Proof

Step	Hyp	Ref	Expression
1		csbie2df.p	$$⊢Ⅎx\phi$$
2		csbie2df.c	$$⊢\phi \to \underset{\_}{Ⅎ}xC$$
3		csbie2df.d	$$⊢\phi \to \underset{\_}{Ⅎ}xD$$
4		csbie2df.a	$$⊢\phi \to A\in V$$
5		csbie2df.1	$$⊢\left(\phi \wedge x=y\right)\to B=C$$
6		csbie2df.2	$$⊢\left(\phi \wedge y=A\right)\to C=D$$
7		eqidd	$$⊢\phi \to D=D$$
8		dfsbcq	$$⊢y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}B=D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=D\right)$$
9		sbceqg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=D\leftrightarrow ⦋A/x⦌B=⦋A/x⦌D\right)$$
10	9	adantr	$$⊢\left(A\in V\wedge \phi \right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=D\leftrightarrow ⦋A/x⦌B=⦋A/x⦌D\right)$$
11		csbtt	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}xD\right)\to ⦋A/x⦌D=D$$
12	3 11	sylan2	$$⊢\left(A\in V\wedge \phi \right)\to ⦋A/x⦌D=D$$
13	12	eqeq2d	$$⊢\left(A\in V\wedge \phi \right)\to \left(⦋A/x⦌B=⦋A/x⦌D\leftrightarrow ⦋A/x⦌B=D\right)$$
14	10 13	bitrd	$$⊢\left(A\in V\wedge \phi \right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=D\leftrightarrow ⦋A/x⦌B=D\right)$$
15	4 14	mpancom	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=D\leftrightarrow ⦋A/x⦌B=D\right)$$
16	8 15	sylan9bb	$$⊢\left(y=A\wedge \phi \right)\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}B=D\leftrightarrow ⦋A/x⦌B=D\right)$$
17	16	pm5.74da	$$⊢y=A\to \left(\left(\phi \to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}B=D\right)\leftrightarrow \left(\phi \to ⦋A/x⦌B=D\right)\right)$$
18	6	eqeq1d	$$⊢\left(\phi \wedge y=A\right)\to \left(C=D\leftrightarrow D=D\right)$$
19	18	expcom	$$⊢y=A\to \left(\phi \to \left(C=D\leftrightarrow D=D\right)\right)$$
20	19	pm5.74d	$$⊢y=A\to \left(\left(\phi \to C=D\right)\leftrightarrow \left(\phi \to D=D\right)\right)$$
21		sbsbc	$$⊢\left[y/x\right]B=D\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}B=D$$
22	2 3	nfeqd	$$⊢\phi \to ℲxC=D$$
23	5	eqeq1d	$$⊢\left(\phi \wedge x=y\right)\to \left(B=D\leftrightarrow C=D\right)$$
24	23	ex	$$⊢\phi \to \left(x=y\to \left(B=D\leftrightarrow C=D\right)\right)$$
25	1 22 24	sbiedw	$$⊢\phi \to \left(\left[y/x\right]B=D\leftrightarrow C=D\right)$$
26	21 25	bitr3id	$$⊢\phi \to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}B=D\leftrightarrow C=D\right)$$
27	26	pm5.74i	$$⊢\left(\phi \to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}B=D\right)\leftrightarrow \left(\phi \to C=D\right)$$
28	17 20 27	vtoclbg	$$⊢A\in V\to \left(\left(\phi \to ⦋A/x⦌B=D\right)\leftrightarrow \left(\phi \to D=D\right)\right)$$
29	7 28	mpbiri	$$⊢A\in V\to \left(\phi \to ⦋A/x⦌B=D\right)$$
30	4 29	mpcom	$$⊢\phi \to ⦋A/x⦌B=D$$