Theorem sbc2iedf

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

	Ref	Expression
Hypotheses	sbc2iedf.1	⊢ Ⅎ 𝑥 𝜑
	sbc2iedf.2	⊢ Ⅎ 𝑦 𝜑
	sbc2iedf.3	⊢ Ⅎ 𝑥 𝜒
	sbc2iedf.4	⊢ Ⅎ 𝑦 𝜒
	sbc2iedf.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sbc2iedf.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	sbc2iedf.7	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	sbc2iedf	⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		sbc2iedf.1	⊢ Ⅎ 𝑥 𝜑
2		sbc2iedf.2	⊢ Ⅎ 𝑦 𝜑
3		sbc2iedf.3	⊢ Ⅎ 𝑥 𝜒
4		sbc2iedf.4	⊢ Ⅎ 𝑦 𝜒
5		sbc2iedf.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		sbc2iedf.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
7		sbc2iedf.7	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
8	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝑊 )
9	7	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
10		nfv	⊢ Ⅎ 𝑦 𝑥 = 𝐴
11	2 10	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 )
12	4	a1i	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → Ⅎ 𝑦 𝜒 )
13	8 9 11 12	sbciedf	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )
14	3	a1i	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
15	5 13 1 14	sbciedf	⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )