Theorem sbc2iegf

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013)

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

Proof

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