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

Metamath Proof Explorer

Theorem sbc3ie

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

Ref Expression
Hypotheses sbc3ie.1 ⊢ A ∈ V
sbc3ie.2 ⊢ B ∈ V
sbc3ie.3 ⊢ C ∈ V
sbc3ie.4 ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
Assertion sbc3ie ⊢ [˙A / x]˙ [˙B / y]˙ [˙C / z]˙ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 sbc3ie.1 ⊢ A ∈ V
2 sbc3ie.2 ⊢ B ∈ V
3 sbc3ie.3 ⊢ C ∈ V
4 sbc3ie.4 ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
5 3 a1i ⊢ x = A ∧ y = B → C ∈ V
6 4 3expa ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
7 5 6 sbcied ⊢ x = A ∧ y = B → [˙C / z]˙ φ ↔ ψ
8 1 2 7 sbc2ie ⊢ [˙A / x]˙ [˙B / y]˙ [˙C / z]˙ φ ↔ ψ