This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ 𝜓 ) )