Theorem sbc2iedv

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008) (Proof shortened by Mario Carneiro, 18-Oct-2016)

	Ref	Expression
Hypotheses	sbc2iedv.1	⊢ 𝐴 ∈ V
	sbc2iedv.2	⊢ 𝐵 ∈ V
	sbc2iedv.3	⊢ ( 𝜑 → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) ) )
Assertion	sbc2iedv	⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		sbc2iedv.1	⊢ 𝐴 ∈ V
2		sbc2iedv.2	⊢ 𝐵 ∈ V
3		sbc2iedv.3	⊢ ( 𝜑 → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) ) )
4	1	a1i	⊢ ( 𝜑 → 𝐴 ∈ V )
5	2	a1i	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ V )
6	3	impl	⊢ ( ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ∧ 𝑦 = 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
7	5 6	sbcied	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )
8	4 7	sbcied	⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜓 ↔ 𝜒 ) )