Theorem sbc2iedf

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Thierry Arnoux, 4-Jul-2023)

	Ref	Expression
Hypotheses	sbc2iedf.1	$$⊢Ⅎx\phi$$
	sbc2iedf.2	$$⊢Ⅎy\phi$$
	sbc2iedf.3	$$⊢Ⅎx\chi$$
	sbc2iedf.4	$$⊢Ⅎy\chi$$
	sbc2iedf.5	$$⊢\phi \to A\in V$$
	sbc2iedf.6	$$⊢\phi \to B\in W$$
	sbc2iedf.7	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	sbc2iedf	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbc2iedf.1	$$⊢Ⅎx\phi$$
2		sbc2iedf.2	$$⊢Ⅎy\phi$$
3		sbc2iedf.3	$$⊢Ⅎx\chi$$
4		sbc2iedf.4	$$⊢Ⅎy\chi$$
5		sbc2iedf.5	$$⊢\phi \to A\in V$$
6		sbc2iedf.6	$$⊢\phi \to B\in W$$
7		sbc2iedf.7	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
8	6	adantr	$$⊢\left(\phi \wedge x=A\right)\to B\in W$$
9	7	anassrs	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to \left(\psi \leftrightarrow \chi \right)$$
10		nfv	$$⊢Ⅎyx=A$$
11	2 10	nfan	$$⊢Ⅎy\left(\phi \wedge x=A\right)$$
12	4	a1i	$$⊢\left(\phi \wedge x=A\right)\to Ⅎy\chi$$
13	8 9 11 12	sbciedf	$$⊢\left(\phi \wedge x=A\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
14	3	a1i	$$⊢\phi \to Ⅎx\chi$$
15	5 13 1 14	sbciedf	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$